+set "baseuri" "cic:/matita/tests/match_inference/".
+
inductive pos: Set \def
| one : pos
| next : pos \to pos.
match (le_n O) with
[ le_n \Rightarrow I
| (le_S y p') \Rightarrow I ].
+
+inductive Prod (A,B:Set): Set \def
+pair : A \to B \to Prod A B.
+
+definition fst : \forall A,B:Set. (Prod A B) \to A \def
+\lambda A,B:Set. \lambda p:(Prod A B). match p with
+[(pair a b) \Rightarrow a].