diff --git a/_CoqProject b/_CoqProject
index 25fe83e1cfe64da1f3b7dce2fb0a0b8d8cc910d1..cde1fc11d08531e21e671d6d5f919415764cee39 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,4 +10,5 @@ theories/GQMDedSubst.v
 theories/GQMTactics.v
 theories/Section5.v
 theories/Section5WithContext.v
+theories/Section7.v
 lib/LibTactics.v
\ No newline at end of file
diff --git a/theories/Section5.v b/theories/Section5.v
index 5a090f306b71cc2092da3ad5cb2d877b1ac19d51..29d003e48c72103eefd0919fd3cc0547f4df9d7f 100644
--- a/theories/Section5.v
+++ b/theories/Section5.v
@@ -445,7 +445,7 @@ Proof.
   hSplit.
   - apply: lemma_A_5_1_2.
       by apply: lemma_A_7_4.
-  - rewrite /SquareExists /DiamondExists.
+  - rewrite /SquareExists.
     apply: (tac_rewrite (fun X => _ ->> -! ([A] -! X)) (lemma_A_7_8_1 _)).
     apply: gqm_id.
 Qed.
diff --git a/theories/Section7.v b/theories/Section7.v
new file mode 100644
index 0000000000000000000000000000000000000000..abd33fff147485a11b5ae545e0443b960defac3c
--- /dev/null
+++ b/theories/Section7.v
@@ -0,0 +1,54 @@
+(** * Proofs for Section 7
+everything here is based on the numbering in the extendend report
+*)
+
+Require Import GQM.Base.
+Require Import GQM.GQM.
+Require Import GQM.GQMDeduction.
+Require Import GQM.GQMClassicalWithTactics.
+Require Import GQM.Section5.
+
+(** ** Lemma A.8 *)
+Lemma lemma_A_8_1 : forall A B, |-- (|A| A & [A]B) <<->> [A](A.[ren (+1)] & B).
+Proof.
+  move => A B.
+  hSplit.
+  - (* (5) *)
+    apply: (tac_rewriteR (fun X => _ ->> X) (lemma_A_7_9_1 _)).
+    (* (4) *)
+    apply: gqm_univgen.
+    (* (3) *)
+    apply (tac_rewrite (fun X => _ ->> X) (lemma_A_7_2_1 _ _)).
+    (* (2) *)
+    rewrite /All.
+    asimpl.
+    rewrite !ids_0_neg -/(And ([A] A._[ren_ (+2)]) ([A] B._[ren_ (0 .: (+2))])).
+    apply: (tac_rewrite (fun X => X) (gqm_andImpEquiv _ _ _)).
+    apply: gqm_mp; first by apply: gqm_swap.
+    apply: (tac_rewrite (fun X => _ ->> _ ->> X) (gqm_andCom _ _)).
+    apply: gqm_mp; first by apply: gqm_mp; by [apply: (gqm_chain _ ([A] B.[ren (+1)])) | apply: gqm_andI].
+    (* (1) *)
+    have H := (gqm_Aglob (B._[ren_ (0 .: (+2))]) (Var 0)).
+    by asimpl in H.
+  - (* (6) *)
+    have H6 := (gqm_andE1 (A._[ren_ (+1)]) B).
+    (* (7) *)
+    have {H6} H7 := (lemma_A_5_1_1 _ _ H6).
+    (* (8) *)
+    have H8 := (gqm_Aglob (A._[ren_ (+1)]) (Var 0)).
+    asimpl in H8.
+    (* (9) *)
+    have {H7 H8} H9 : (|-- [A] (A.[ren (+1)] & B) ->> [A] A.[ren (+1)]). {
+      apply: gqm_mp; last by apply: H8.
+      by apply: gqm_mp; first by apply: gqm_chain2.
+    }
+    (* (10) *)
+    have H10 := (gqm_andE2 (A._[ren_ (+1)]) B).
+    (* (11) *)
+    have {H10} H11 := (lemma_A_5_1_1 _ _ H10).
+    apply: gqm_mp; last by apply: H11.
+    apply: gqm_mp; first by apply: gqm_I2.
+    apply: gqm_mp; last by apply: H9.
+    apply: gqm_mp; first by apply: gqm_chain.
+    by apply: gqm_andI.
+Qed.
\ No newline at end of file