-(*
-theorem test5: nat → ∃n. 0 ≤ n.
- apply (λn:nat.?);
- apply
- (match n return λ_.∃n.0 ≤ n with [O ⇒ (0 : ∃n.0 ≤ n) | S n' ⇒ ex_intro ? ? n' ?]
- : ∃n. 0 ≤ n);
- autobatch.
+theorem test5: nat → ∃n. 1 ≤ n.
+apply (
+ let rec aux n : nat ≝
+ match n with
+ [ O ⇒ 1
+ | S m ⇒ S (aux m)
+ ]
+ in
+ aux
+: nat → ∃n. 1 ≤ n);
+[ cases (aux n1); simplify; ] autobatch;
+qed.
+
+inductive NN (A:Type) : nat -> Type ≝
+ | NO : NN A O
+ | NS : ∀n:nat. NN A n → NN A (S n).
+
+definition injectN ≝ λA,k.λP.λa:NN A k.λp:P a. sigma_intro ? P ? p.
+
+coercion cic:/matita/tests/coercions_propagation/injectN.con 0 1.
+
+definition ejectN ≝ λA,k.λP.λc: ∃n:NN A k.P n. match c with [ sigma_intro w _ ⇒ w].
+
+coercion cic:/matita/tests/coercions_propagation/ejectN.con.
+
+definition PN :=
+ λA,k.λx:NN A k. 1 <= k.
+
+theorem test51_byhand: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
+intros 1;
+apply (
+ let rec aux (w : nat) (n : NN A w) on n : ∃p:NN A (S w).PN ? ? p ≝
+ match n in NN return λx.λm:NN A x.∃p:NN A (S x).PN ? ? p with
+ [ NO ⇒ injectN ? ? ? (NS A ? (NO A)) ?
+ | NS x m ⇒ injectN ? ? ? (NS A (S x) (ejectN ? ? ? (aux ? m))) ?
+ ]
+ in
+ aux
+: ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m);
+[2: cases (aux x m); simplify; autobatch ] unfold PN; autobatch;