diff --git a/theories/Section5.v b/theories/Section5.v
index f8625d9d4829edb63b78ea8199a2c49c41d3fe25..9fac85cc3516ec8c25e5a799ce63b221178bec30 100644
--- a/theories/Section5.v
+++ b/theories/Section5.v
@@ -249,6 +249,8 @@ Qed.
 
 (** ** Lemma A.6 *)
 
+(** *** Lemma A.6 (i) *)
+
 Lemma lemma_A_6_1_1 : forall A, |-- [A]A ->> [E] A.
 Proof.
   move => A.
@@ -269,6 +271,8 @@ Proof.
   by apply: lemma_A_6_1_1.
 Qed.
 
+(** *** Lemma A.6 (ii) *)
+
 Lemma lemma_A_6_2_1 : forall A, |-- [E](A.[ren (+1)]) ->> [A](A.[ren (+1)]).
 Proof.
   move => A.
@@ -287,6 +291,8 @@ Proof.
   by asimpl in H.
 Qed.
 
+(** *** Lemma A.6 (iii) *)
+
 Lemma lemma_A_6_3_1 : forall A, |-- [A]A ->> <A>A.
 Proof.
   move => A.
@@ -309,12 +315,16 @@ Qed.
 
 (** ** Lemma 5.4 / A.7 *)
 
+(** *** Lemma A.7 (i) *)
+
 Lemma lemma_A_7_1 : forall A B, |-- |A|(A ->> B) ->> (|A|A ->> |A|B).
 Proof.
   move => A B.
     by apply: gqm_ADist.
 Qed.
 
+(** *** Lemma A.7 (ii) *)
+
 Lemma lemma_A_7_2_1 : forall A B, |-- |A|(A & B) <<->> (|A|A & |A| B).
 Proof.
   move => A B.
@@ -338,6 +348,8 @@ Proof.
   apply: lemma_A_7_2_1.
 Qed.
 
+(** *** Lemma A.7 (iii) *)
+
 Lemma lemma_A_7_3_1 : forall A B, |-- A ->> B -> |-- |A|A ->> |A|B.
 Proof.
   move => A B H.
@@ -355,6 +367,8 @@ Proof.
   by apply: gqm_mp; first by apply: gqm_contrap.
 Qed.
 
+(** *** Lemma A.7 (iv) *)
+
 Lemma lemma_A_7_4 : forall A, |-- |A|A ->> A.
 Proof.
   move => A.
@@ -362,6 +376,8 @@ Proof.
   by asimpl in H.
 Qed.
 
+(** *** Lemma A.7 (v) *)
+
 Lemma lemma_A_7_5 : forall A, |-- A ->> |E|A.
 Proof.
   move => A.
@@ -370,11 +386,15 @@ Proof.
     by apply: lemma_A_7_4.
 Qed.
 
+(** *** Lemma A.7 (vi) *)
+
 Lemma lemma_A_7_6 : forall A, |-- |E|A <<->> |A||E|A.
 Proof.
   hSplit; by [apply: gqm_Q5 | apply: lemma_A_7_4].
 Qed.
 
+(** *** Lemma A.7 (vii) *)
+
 Lemma lemma_A_7_7 : forall A, |-- |E||A|A <<->> |A|A.
 Proof.
   move => A.
@@ -384,6 +404,8 @@ Proof.
     by apply: gqm_Q5.
 Qed.
 
+(** *** Lemma A.7 (viii) *)
+
 Lemma lemma_A_7_8_1 : forall A, |-- |A||A|A <<->> |A|A.
 Proof.
   move => A.
@@ -403,3 +425,186 @@ Proof.
   apply: (tac_rewrite (fun X => X ->> _) (lemma_A_7_7 _)).
   apply: gqm_id.
 Qed.
+
+(** *** Lemma A.7 (ix) *)
+
+Lemma lemma_A_7_9_1 : forall A, |-- [A]|A|A <<->> [A]A.
+Proof.
+  move => A.
+  hSplit.
+  - apply: lemma_A_5_1_1.
+      by apply: lemma_A_7_4.
+  - apply: gqm_univgen.
+    asimpl.
+    have H := (gqm_Aglob (A._[ren_ (0.: (+2))]) (Var 0)).
+      by asimpl in H.
+Qed.
+
+Lemma lemma_A_7_9_2 : forall A, |-- [E]|A|A <<->> [E]A.
+Proof.
+  move => A.
+  hSplit.
+  - apply: lemma_A_5_1_2.
+      by apply: lemma_A_7_4.
+  - rewrite /SquareExists /DiamondExists.
+    apply: (tac_rewrite (fun X => _ ->> -! ([A] -! X)) (lemma_A_7_8_1 _)).
+    apply: gqm_id.
+Qed.
+
+Lemma lemma_A_7_9_3 : forall A, |-- <A>|A|A <<->> [A]A.
+Proof.
+  move => A.
+  hSplit.
+  - rewrite /DiamondAll.
+    apply: (tac_rewrite (fun X => [A] X ->> _) (lemma_A_7_7 _)).
+    apply: lemma_A_5_1_1.
+      by apply: lemma_A_7_4.
+  - apply: gqm_mp; last by apply: (lemma_A_6_3_1 (|A| A)).
+    apply: gqm_mp; first by apply: gqm_chain2.
+    apply: gqm_univgen.
+    asimpl.
+    have H := (gqm_Aglob (A._[ren_ (0.: (+2))]) (Var 0)).
+      by asimpl in H.
+Qed.
+
+Lemma lemma_A_7_9_4 : forall A, |-- <E>|A|A <<->> [E]A.
+Proof.
+  move => A.
+  rewrite /SquareExists /DiamondExists.
+  apply: gqm_idEquiv.
+Qed.
+
+(** *** Lemma A.7 (x) *)
+
+Lemma lemma_A_7_10_3 : forall A, |-- <A>|E|A <<->> <A>A.
+Proof.
+  move => A.
+  hSplit.
+  - rewrite /DiamondAll.
+    apply: (tac_rewrite (fun X => [A] X ->> _) (lemma_A_7_8_2 _)).
+      by apply: gqm_id.
+  - apply: lemma_A_5_2_1.
+    by apply: lemma_A_7_5.
+Qed.
+
+Lemma lemma_A_7_10_4 : forall A, |-- <E>|E|A <<->> <E>A.
+Proof.
+  move => A.
+  hSplit.
+  - rewrite /DiamondExists /Exists.
+    apply: (tac_rewriteR (fun X => -! ([A] X) ->> _) (gqm_dnegEquiv _)).
+    apply: gqm_mp; first by apply: gqm_contrap.
+    by hAndDestruct (lemma_A_7_9_1 (-! A)).
+  - apply: lemma_A_5_2_2.
+    by apply: lemma_A_7_5.
+Qed.
+
+Lemma lemma_A_7_10_1 : forall A, |-- [A]|E|A <<->> <A>A.
+Proof.
+  move => A.
+  rewrite /DiamondAll.
+  by apply: gqm_idEquiv.
+Qed.
+
+Lemma lemma_A_7_10_2 : forall A, |-- [E]|E|A <<->> <E>A.
+Proof.
+  move => A.
+  rewrite /SquareExists.
+  apply: (tac_rewriteR (fun X => <E> X <<->> _) (lemma_A_7_6 _)).
+  by apply: lemma_A_7_10_4.
+Qed.
+
+(** *** Lemma A.7 (xi) *)
+
+Lemma lemma_A_7_11_1 : forall A, |-- [A]A <<->> |A|[A]A.
+Proof.
+  move => A.
+  hSplit; last by apply: lemma_A_7_4.
+  apply: gqm_univgen.
+  asimpl.
+  by apply: gqm_id.
+Qed.
+
+Lemma lemma_A_7_11_2 : forall A, |-- [E]A <<->> |A|[E]A.
+Proof.
+  move => A.
+  hSplit; last by apply: lemma_A_7_4.
+  rewrite /SquareExists /DiamondExists.
+  by apply: gqm_Q5.
+Qed.
+
+Lemma lemma_A_7_11_3 : forall A, |-- <A>A <<->> |A|<A>A.
+Proof.
+  move => A.
+  hSplit; last by apply: lemma_A_7_4.
+  (* (6) *)
+  rewrite /DiamondAll /Exists.
+  apply: gqm_mp; first by apply: gqm_I3.
+  apply: (tac_rewrite (fun X => -! (|A| X) ->> -! ([A] -! (|A| -! A))) (gqm_dnegEquiv _)).
+  fold (DiamondExists (|A| -! A)) (Exists (<E> |A| -! A)) (SquareExists (-! A)).
+  (* (5) *)
+  apply: gqm_mp; last by apply: (lemma_A_7_4 ([E] -! A)).
+  apply: gqm_mp; first by apply: gqm_chain2.
+  apply: (tac_rewriteR (fun X => _ ->> X ) (lemma_A_7_7 _)).
+  (* (4) *)
+  apply: lemma_A_7_3_2.
+  (* (3) *)
+  by hAndDestruct (lemma_A_7_11_2 (-! A)).
+Qed.
+
+Lemma lemma_A_7_11_4 : forall A, |-- <E>A <<->> |A|<E>A.
+Proof.
+  move => A.
+  hSplit; last by apply: lemma_A_7_4.
+  (* (6) *)
+  rewrite /DiamondExists.
+  apply: gqm_mp; first by apply: gqm_I3.
+  fold (Exists ([A] -! A)).
+  apply: (tac_rewriteR (fun X => _ ->> X) (gqm_dnegEquiv _)).
+  (* (5) *)
+  apply: gqm_mp; last by apply: (lemma_A_7_4 ([A] -! A)).
+  apply: gqm_mp; first by apply: gqm_chain2.
+  apply: (tac_rewriteR (fun X => _ ->> X ) (lemma_A_7_7 _)).
+  (* (4) *)
+  apply: lemma_A_7_3_2.
+  (* (3) *)
+  by hAndDestruct (lemma_A_7_11_1 (-! A)).
+Qed.
+
+(** *** Lemma A.7 (xii) *)
+
+Lemma lemma_A_7_12_1 : forall A, |-- [A]A <<->> |E|[A]A.
+Proof.
+  move => A.
+  rewrite /Exists.
+  apply: (tac_rewrite (fun X => X) (gqm_equivNegEquiv2 _ _)).
+  apply: (tac_rewrite (fun X => -! ([A] X) <<->> |A| -! ([A] X)) (gqm_dnegEquiv _)).
+    by apply: lemma_A_7_11_4.
+Qed.
+
+Lemma lemma_A_7_12_2 : forall A, |-- [E]A <<->> |E|[E]A.
+Proof.
+  move => A.
+  rewrite /Exists /SquareExists /DiamondExists.
+  apply: (tac_rewriteR (fun X => X) (gqm_equivNegEquiv _ _)).
+  apply: (tac_rewriteR (fun X => _ <<->> |A| X) (gqm_dnegEquiv _)).
+    by apply: lemma_A_7_11_1.
+Qed.
+
+Lemma lemma_A_7_12_3 : forall A, |-- <A>A <<->> |E|<A>A.
+Proof.
+  move => A.
+  rewrite /Exists /DiamondAll.
+  apply: (tac_rewrite (fun X => X) (gqm_equivNegEquiv2 _ _)).
+  apply: (tac_rewrite (fun X => -! ([A] X) <<->> |A| -! ([A] X)) (gqm_dnegEquiv _)).
+    by apply: lemma_A_7_11_4.
+Qed.
+
+Lemma lemma_A_7_12_4 : forall A, |-- <E>A <<->> |E|<E>A.
+Proof.
+  move => A.
+  rewrite /Exists /SquareExists /DiamondExists.
+  apply: (tac_rewriteR (fun X => X) (gqm_equivNegEquiv _ _)).
+  apply: (tac_rewriteR (fun X => _ <<->> |A| X) (gqm_dnegEquiv _)).
+    by apply: lemma_A_7_11_1.
+Qed.
\ No newline at end of file