(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/injection".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
theorem injection_test0: ∀n,n',m,m'. k0 n m = k0 n' m' → m = m'.
intros;
destruct H;
- assumption.
+ reflexivity.
qed.
inductive t : Type → Type :=
theorem injection_test1: ∀n,n'. k n = k n' → n = n'.
intros;
destruct H;
- assumption.
+ reflexivity.
qed.
inductive tt (A:Type) : Type -> Type :=
theorem injection_test2: ∀n,n',m,m'. k1 bool n n' = k1 bool m m' → n' = m'.
intros;
destruct H;
- assumption.
+ reflexivity.
qed.
inductive ttree : Type → Type :=
∀n,n',m,m'. k1 bool (S n) (S (S m)) = k1 bool (S n') (S (S (S m'))) → m = S m'.
intros;
destruct H;
- assumption.
+ reflexivity.
qed.