X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fsets.ma;h=4d77f6c2f86f5808bbdbe6e416ca6676969e6f86;hb=ef3bdc4be26f6518a82a79c64e986253f7aeaa3c;hp=bb077e65384db670bc10bb4fe184cf8c92ee6d46;hpb=844794906f5a9f97406d72b5305ce13fb75acf94;p=helm.git

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.