in this way. For instance, the sum of two natural numbers can be defined as
follows: *)
-let rec add n m ≝
+let rec add n (m:nat) ≝
match n with
[ O ⇒ m
| S a ⇒ S (add a m)
example quotient8: witness … (div2Pagain (twice (twice (twice (twice (S O))))))
= 〈twice (twice (twice (S O))), ff〉.
// qed.
+
+(********************)
+
+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 @(mk_Sub … (add a b))
+elim Ha
+ [normalize @Hb
+ |#x #Hx #Hind normalize @pari2 @Hind
+ ]
+qed.
+