+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;