From 2327897158cc01b63c68d3b82872c17159fbb8e6 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 3 Jan 2012 15:57:18 +0000
Subject: [PATCH] more properties of union

---
 matita/matita/lib/basics/sets.ma | 5 +++++
 1 file changed, 5 insertions(+)

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. 
-- 
2.39.2