From 19784f5cbda302eabb97c69e152e8cc9870e783c Mon Sep 17 00:00:00 2001
From: Mackie Loeffel <mackie.loeffel@web.de>
Date: Fri, 4 May 2018 19:17:49 +0200
Subject: [PATCH] lemma A 8 (viii)

---
 theories/Section5.v | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/theories/Section5.v b/theories/Section5.v
index 09c8466..f8625d9 100644
--- a/theories/Section5.v
+++ b/theories/Section5.v
@@ -378,12 +378,28 @@ Qed.
 Lemma lemma_A_7_7 : forall A, |-- |E||A|A <<->> |A|A.
 Proof.
   move => A.
+  hSplit; last by apply: lemma_A_7_5.
   rewrite /Exists.
-  (* TODO finish *)
-Abort.
+  apply: gqm_mp; first by apply: gqm_contrap2.
+    by apply: gqm_Q5.
+Qed.
 
 Lemma lemma_A_7_8_1 : forall A, |-- |A||A|A <<->> |A|A.
 Proof.
   move => A.
-  rewrite /Exists.
-Abort.
+  hSplit; first by apply: lemma_A_7_4.
+  apply: (tac_rewriteR (fun X => X ->> _) (lemma_A_7_7 _)).
+  apply: (tac_rewrite (fun X => X ->> _) (lemma_A_7_6 _)).
+  apply: (tac_rewrite (fun X => |A|X ->> _) (lemma_A_7_7 _)).
+  apply: gqm_id.
+Qed.
+
+Lemma lemma_A_7_8_2 : forall A, |-- |E||E|A <<->> |E|A.
+Proof.
+  move => A.
+  hSplit; last by apply: lemma_A_7_5.
+  apply: (tac_rewrite (fun X => _ ->> X) (lemma_A_7_6 _)).
+  apply: (tac_rewrite (fun X => |E|X ->> _) (lemma_A_7_6 _)).
+  apply: (tac_rewrite (fun X => X ->> _) (lemma_A_7_7 _)).
+  apply: gqm_id.
+Qed.
-- 
GitLab