+
+(********************)
+
+inductive Pari : nat → Prop ≝
+ | pariO : Pari O
+ | pari2 : ∀x. Pari x → Pari (S (S x)).
+
+definition natPari ≝ Sub nat Pari.
+
+definition addPari: natPari → natPari → natPari.
+* #a #Ha * #b #Hb check mk_Sub @(mk_Sub … (add a b))
+elim Ha
+ [normalize @Hb
+ |#x #Hx #Hind normalize @pari2 @Hind
+ ]
+qed.
+