Skip to content
Snippets Groups Projects

solve_ndisj: handle goals containing _ ∖ _ ∖ _

Merged solve_ndisj: handle goals containing _ ∖ _ ∖ _
ralf/solve_ndisj into master
All threads resolved!
Merged Ralf Jung requested to merge ralf/solve_ndisj into master
All threads resolved!
Compare
and
3 files
+ 18
− 8
Compare changes
  • Side-by-side
  • Inline
Files
3
tests/solve_ndisj.v
+ 4
− 0
@@ -43,3 +43,7 @@ Proof. solve_ndisj. Qed.
Lemma test9 N1 N2 :
⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter" ∖ ↑N1.@"state" ∖ ↑N2.
Proof. solve_ndisj. Qed.
Lemma test10 N1 N2 E :
↑N1 ∪ E ## ⊤ ∖ ↑N1 ∖ ↑N2 ∖ E.
Proof. solve_ndisj. Qed.