- lambda: some parts commented out, some refactoring

[helm.git] / matita / matita / lib / basics / logic.ma

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 76b4239d4a537037c73ea6649e19fa94c81cdd36..4b90f75181300bdaced20673e08e5d6420f4fbc1 100644 (file)
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -153,7 +153,7 @@ interpretation "exists on two predicates" 'exists2 x1 x2 = (ex2 ? x1 x2).
 
 lemma ex2_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
 #A0 #P0 #P1 * /2 width=3/
-qed.
+qed-.
 
 (* iff *)
 definition iff :=