Skip to content
Snippets Groups Projects

make solve_ndisj more powerful

Merged make solve_ndisj more powerful
ralf/solve_ndisj into master
Merged Ralf Jung requested to merge ralf/solve_ndisj into master
Compare
and
Show latest version
1 file
+ 3
− 1
Compare changes
  • Side-by-side
  • Inline
theories/sets.v
+ 3
− 1
@@ -666,7 +666,9 @@ Section set.
Proof. set_solver. Qed.
Lemma disjoint_difference_l2 X1 X2 Y : X1 ## Y → X1 ∖ X2 ## Y.
Proof. set_solver. Qed.
Lemma disjoint_difference_r X Y1 Y2 : X ⊆ Y2 ∨ X ## Y1 → X ## Y1 ∖ Y2.
Lemma disjoint_difference_r1 X Y1 Y2 : X ⊆ Y2 → X ## Y1 ∖ Y2.
Proof. set_solver. Qed.
Lemma disjoint_difference_r2 X Y1 Y2 : X ## Y1 → X ## Y1 ∖ Y2.
Proof. set_solver. Qed.
Section leibniz.