(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/injection/".
+set "baseuri" "cic:/matita/tests/injection".
-include "legacy/coq.ma".
+include "../legacy/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;
- injection H;
+ destruct H;
assumption.
qed.
theorem injection_test1: ∀n,n'. k n = k n' → n = n'.
intros;
- injection H;
+ destruct H;
assumption.
qed.
theorem injection_test2: ∀n,n',m,m'. k1 bool n n' = k1 bool m m' → n' = m'.
intros;
- injection H;
+ destruct H;
assumption.
qed.
tempty: ttree nat
| tnode : ∀A. ttree A → ttree A → ttree A.
-theorem injection_test3:
- ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'.
- intros;
- injection H;
- assumption.
-qed.
-
-theorem injection_test3:
- ∀t,t'.
- tnode nat (tnode nat t t') tempty = tnode nat (tnode nat t' tempty) tempty →
- t = t'.
- intros;
- injection H;
-
-
theorem injection_test4:
- ∀n,n',m,m'. k1 bool (S n) (S m) = k1 bool (S n') (S (S m')) → m = S m'.
+ ∀n,n',m,m'. k1 bool (S n) (S (S m)) = k1 bool (S n') (S (S (S m'))) → m = S m'.
intros;
- injection H;
+ destruct H;
assumption.
qed.
-
-