lemma A 8 (viii)

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.