From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 3 Jan 2012 15:57:18 +0000 (+0000)
Subject: more properties of union
X-Git-Tag: make_still_working~1994
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2327897158cc01b63c68d3b82872c17159fbb8e6;p=helm.git

more properties of union
---

diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma
index bb077e653..4d77f6c2f 100644
--- a/matita/matita/lib/basics/sets.ma
+++ b/matita/matita/lib/basics/sets.ma
@@ -74,6 +74,11 @@ lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
 
 (* set equalities *)
+lemma union_empty_r: ∀U.∀A:U→Prop. 
+  A ∪ ∅ =1 A.
+#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
+qed.
+
 lemma union_comm : ∀U.∀A,B:U →Prop. 
   A ∪ B =1 B ∪ A.
 #U #A #B #a % * /2/ qed.