nat_rectぐらいなら、数学的帰納法なんてなじみがあるからなんとなくわかるけど、 例えば Inductive sand (A B : Set) : Set := sconj : A -> B -> sand A B. から作られるsand_rectなんかは、
sand_rect = fun (A B : Set) (P : sand A B -> Type) (f : forall (a : A) (b : B), P (sconj A B a b)) (s : sand A B) => match s as s0 return (P s0) with | sconj x x0 => f x x0 end : forall (A B : Set) (P : sand A B -> Type), (forall (a : A) (b : B), P (sconj A B a b)) -> forall s : sand A B, P s
