Skip to content
Snippets Groups Projects
Commit 46636b6f authored by Mackie Loeffel's avatar Mackie Loeffel
Browse files

use dneg_equiv

parent c91b880f
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 6 deletions
theories/Section5.v
+ 2
− 6
View file @ 46636b6f
......@@ -27,12 +27,8 @@ Qed.
Lemma lemma_A_2_2 : forall A, |-- <A>A <<->> -![E]-!A.
Proof.
move => A.
rewrite /DiamondAll /SquareExists /Exists.
hSplit.
- apply: gqm_mp; first by apply: gqm_contrap3.
by hAndDestruct (lemma_A_2_1 (|A| -! A)).
- apply: gqm_mp; first by apply: gqm_contrap2.
by hAndDestruct (lemma_A_2_1 (|A| -! A)).
rewrite /DiamondAll /SquareExists /Exists /DiamondExists.
apply: gqm_dnegEquiv.
Qed.
Lemma lemma_A_2_3 : forall A, |-- [A]A <<->> -!<E>-!A.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment