Commit 4fd8d550 by Robbert Krebbers

Fix more _L lemmas.

parent 108d1f8d
 ... @@ -643,9 +643,9 @@ Section collection. ... @@ -643,9 +643,9 @@ Section collection. Proof. unfold_leibniz; apply union_intersection_l. Qed. Proof. unfold_leibniz; apply union_intersection_l. Qed. Lemma union_intersection_r_L X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z). Lemma union_intersection_r_L X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z). Proof. unfold_leibniz; apply union_intersection_r. Qed. Proof. unfold_leibniz; apply union_intersection_r. Qed. Lemma intersection_union_l_L X Y Z : X ∩ (Y ∪ Z) ≡ (X ∩ Y) ∪ (X ∩ Z). Lemma intersection_union_l_L X Y Z : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z). Proof. unfold_leibniz; apply intersection_union_l. Qed. Proof. unfold_leibniz; apply intersection_union_l. Qed. Lemma intersection_union_r_L X Y Z : (X ∪ Y) ∩ Z ≡ (X ∩ Z) ∪ (Y ∩ Z). Lemma intersection_union_r_L X Y Z : (X ∪ Y) ∩ Z = (X ∩ Z) ∪ (Y ∩ Z). Proof. unfold_leibniz; apply intersection_union_r. Qed. Proof. unfold_leibniz; apply intersection_union_r. Qed. (** Difference *) (** Difference *) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!