ported to new syntactic requirement about terms being surrounded by parens

[helm.git] / helm / matita / library / logic / equality.ma

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index a5d2f0d1e461cd5c02e95aa5f2eb1ec04f96d5fd..ed257afa4c3e47c8e6017ee412f38ac97ef6cea1 100644 (file)
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -48,7 +48,7 @@ theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
 theorem eq_elim_r:
  \forall A:Type.\forall x:A. \forall P: A \to Prop.
    P x \to \forall y:A. y=x \to P y.
-intros. elim sym_eq ? ? ? H1.assumption.
+intros. elim (sym_eq ? ? ? H1).assumption.
 qed.
 
 default "equality"
@@ -68,3 +68,20 @@ theorem eq_f2: \forall  A,B,C:Type.\forall f:A\to B \to C.
 x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2.
 intros.elim H1.elim H.reflexivity.
 qed.
+
+(*
+theorem a:\forall x.x=x\land True.
+[ 
+2:intros;
+  split;
+  [
+    exact (refl_eq Prop x);
+  |
+    exact I;
+  ]
+1:
+  skip
+]
+qed.
+*)
+