X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fdecl.ma;fp=helm%2Fsoftware%2Fmatita%2Ftests%2Fdecl.ma;h=e2035d182a11bc87a7bc308e5b4ab18a52ff9cd7;hb=bd277786d78d49594b3ada1c3c9c28cba5dc03b9;hp=285d07c23dafb783c4ddc10e56717b1ba5f348f8;hpb=73284b016dc2c195491ab3442457ec9fb76b576f;p=helm.git

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index 285d07c23..e2035d182 100644
--- a/helm/software/matita/tests/decl.ma
+++ b/helm/software/matita/tests/decl.ma
@@ -71,4 +71,29 @@ theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O.
     ]
   ]
 qed.
-      
\ No newline at end of file
+
+
+theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
+ assume P: Prop.
+ suppose (P ∧ ∃m:nat.m ≠ m) (H).
+ by H we have P (H1) and (∃x:nat.x≠x) (H2).
+ (*BUG:
+ by H2 let q:nat such that (q ≠ q) (Ineq).
+ *)
+ (* the next line is wrong, but for the moment it does the job *)
+ by H2 let q:nat such that False (Ineq).
+ by I done.
+qed.
+
+theorem easy4: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
+assume n: nat.
+assume m:nat.
+assume p:nat.
+suppose (n=m) (H).
+suppose (S m = S p) (K).
+suppose (n = S p) (L).
+obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
+             = (S p) by K.
+             = n by (sym_eq ? ? ? L)
+done.
+qed.