Inductive nat : type := | O : nat | S : V (x: nat). nat. Recursive plus (a: nat) (b: nat) [0] : nat := match a with ( b, \ (a1: nat). S (plus a1 b) ). Inductive eq (A: type) (a: A) : V (b: A). type := | eqrefl: eq A a a. Definition eqind : V (A:type). (V (a:A). (V (P:V (x:A). (type)). (V (Pa:P a). (V (b:A). (V (eqab:eq A a b). (P b)))))) := ( \ (A: type). \ (a: A). \ (P: V (x: A). type). \ (Pa: P a). \ (b: A). \ (eqab: eq A a b) . match eqab return (P b) with ( \ (A: type). \ (a: A). Pa ) ). Lemma eqcomm: V (A: type). V(a: A). V(b: A). V (H: eq A a b). eq A b a. intro. intro. intro. intro. factorize b. apply eqind. exact A. exact a. simpl. apply eqrefl. apply H. Qed. Lemma eqSnat: V (a: nat). V (b: nat). V (eqab: eq nat a b). eq nat (S a) (S b). intro. intro. intro. factorize b. apply eqind. exact nat. exact a. simpl. apply eqrefl. apply eqab. Qed. Lemma plusOcomm: V (a: nat). eq nat a (plus a O). intro. factorize a. apply natinduc. simpl. apply eqrefl. intro. intro. simpl in Predindind10. simpl. apply eqSnat. exact Predindind10. Qed. Lemma plusSnat: V (a: nat). V (b: nat). eq nat (plus a (S b)) (S (plus a b)). intro. intro. factorize a. apply natinduc. simpl. apply eqrefl. simpl. intro. intro. apply eqSnat. apply Predindind10. Qed. Lemma pluscomm: V (a: nat). V (b: nat). eq nat (plus a b) (plus b a). intro. intro. factorize a. apply natinduc. simpl. apply plusOcomm. intro. intro. simpl. simpl in Predindind10. factorize (plus b (S x0)). apply eqind. exact nat. exact (S (plus b x0)). simpl. apply eqSnat. apply Predindind10. apply eqcomm. apply plusSnat. Qed. Extract Def.