11/11/12 12:04:00.72
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
となって、わかりそうなわからなそうな。上記のSetをPropにかえるともうお手上げ。
いったい何を理解すればいいのやら。どうか神様教えて。