diff --git a/theories/GQM.v b/theories/GQM.v
index e25f8a130be2fd7e7f19a4de346e943973be8982..4b025cb9549f016e2e839225f03917a97fb8f442 100644
--- a/theories/GQM.v
+++ b/theories/GQM.v
@@ -18,6 +18,7 @@ Notation "A '->>' B" := (Imp A B) (at level 77, right associativity).
 Definition Bot := [A] (Var 0).
 Definition Neg A := A ->> Bot.
 Notation "'-!' A" := (Neg A) (at level 73, right associativity).
+Definition Top := -! Bot.
 
 Definition Or A B := (-! A ->> B).
 Definition And A B := -! ( A ->> -! B).
diff --git a/theories/GQMClassical.v b/theories/GQMClassical.v
index a64475f7ca84e443315bb3ffa8d2a3d3eced8938..6597dbde02b9004658faab776d91bb1ab5b18452 100644
--- a/theories/GQMClassical.v
+++ b/theories/GQMClassical.v
@@ -34,6 +34,10 @@ Lemma gqm_id'' : forall A, |-- (A ->> A).
   by apply: gqm_I2.
 Qed.
 
+Lemma gqm_topI : |-- Top.
+  apply: gqm_id.
+Qed.
+
 Lemma gqm_appl : forall A B, |-- ((A ->> B) ->> A ->> B).
 Proof.
   eauto with GQMDB.
@@ -66,6 +70,16 @@ Proof.
   by apply: gqm_chain.
 Qed.
 
+Lemma gqm_3chain : forall A B C D, |-- (C ->> D) ->> (B ->> C) ->> (A ->> B) ->> (A ->> D).
+Proof.
+  move => A B C D.
+  apply: gqm_mp.
+  - apply: gqm_mp; first by apply: (gqm_chain _ ((B ->> C) ->> B ->> D)).
+    apply: gqm_mp; first by apply: gqm_chain.
+    apply: gqm_chain.
+  - apply: gqm_chain.
+Qed.
+
 Lemma gqm_discard : forall A B C, |-- (A ->> C) ->> (B ->> A ->> C).
 Proof.
   eauto with GQMDB.
@@ -274,4 +288,4 @@ Proof.
         apply: ((-! A ->> B) ->> -! A ->> C).
       * apply: gqm_swap.
     + apply: gqm_chain.
-Qed.
+Qed.
\ No newline at end of file
diff --git a/theories/GQMClassicalWithTactics.v b/theories/GQMClassicalWithTactics.v
index 996f0347a676a47619c79f69056a9c69b5e73a79..26f0c9c5a026ac5f56b583d118acc4775ff254f1 100644
--- a/theories/GQMClassicalWithTactics.v
+++ b/theories/GQMClassicalWithTactics.v
@@ -23,4 +23,38 @@ Proof.
   move => A.
   apply: gqm_equiv_comm.
   by apply: gqm_dnegEquiv.
+Qed.
+
+Lemma gqm_impSwapEquiv : forall A B C, |-- (A ->> B ->> C) <<->> (B ->> A ->> C).
+Proof.
+  move => A B C.
+  by hSplit; eauto with GQMDB.
+Qed.
+
+
+Lemma gqm_andImpEquiv : forall A B C, |-- ((A & B) ->> C) <<->> (A ->> B ->> C).
+Proof.
+  move => A B C.
+  hSplit.
+  - apply: gqm_mp; first by apply: gqm_swap.
+    apply: gqm_mp; last by apply: (gqm_andI A B).
+    apply: gqm_mp; first by apply: gqm_chain.
+    apply: gqm_chain2.
+  - apply: gqm_mp; first by apply: gqm_swap.
+    apply: gqm_mp; last by apply: (gqm_andE2 A B).
+    apply: gqm_mp; first by apply: gqm_I2.
+    apply: gqm_mp; last by apply: (gqm_andE1 A B).
+    apply: gqm_mp; first by apply: gqm_chain.
+    hRewrite (gqm_impSwapEquiv B (A ->> B ->> C) C) (fun X => A ->> X).
+    apply: gqm_mp; first by apply: gqm_swap.
+    apply: gqm_id.
+Qed.
+
+Lemma gqm_contrapAndR : forall A B C, |-- ((A & B) ->> C) ->> (A & -! C) ->> -! B.
+Proof.
+  move => A B C.
+  hRewrite (gqm_andImpEquiv A B C) (fun X => X ->> A & -! C ->> -! B).
+  hRewrite (gqm_andImpEquiv A (-!C) (-!B)) (fun X => (A ->> B ->> C) ->>X).
+  apply: gqm_mp; first by apply: gqm_chain.
+  apply: gqm_contrap.
 Qed.
\ No newline at end of file
diff --git a/theories/GQMTactics.v b/theories/GQMTactics.v
index 3e0c778bdb08a940ba88f2a60fd64166bda03b28..2e8b658272b2fd5b6319772aa94d5c0706e5f39c 100644
--- a/theories/GQMTactics.v
+++ b/theories/GQMTactics.v
@@ -33,6 +33,23 @@ Tactic Notation "hAndDestruct" constr(H) := case: (tac_and_destruct_lemma _ _ H)
 
 (** ** hRewrite *)
 
+Lemma tac_rewrite_lem_counter : exists A B r, |-- A <<->> B /\ ~ (|-- (r A) <<->> (r B)).
+Proof.
+  exists (Var 0). exists (-! -! (Var 0)).
+  exists (fun f => match f with
+           | Var n => Bot
+           | _ => -! Bot
+           end).
+  split.
+  - hSplit.
+    + apply: gqm_dnegI.
+    + apply: gqm_dnegE.
+  - move => /= H.
+    hAndDestruct H => _ H.
+    have H2 := (gqm_mp _ _ H gqm_topI); clear H.
+    (* cannot be shown, since |-- is undecidable, but should hold *)
+Abort.
+
 (* Set Typeclasses Debug. *)
 
 Class Rewriteable (X : form -> form) := { form_rewrite : forall A B, |-- A <<->> B -> |-- X A <<->> X B }.
@@ -77,16 +94,23 @@ Proof.
     by have [] := (@imp_r_rewriteable ssrfun.id id_rewriteable X).
 Qed.
 
-(* Instance imp_both_rewriteable(r1 : form -> form)(r2 : form -> form) `{Rewriteable r1} `{Rewriteable r2} (X :form) : Rewriteable (fun B => r1 B ->> r2 B) := {}. *)
-(* Proof. *)
-  (* case: H => Hr1. *)
-  (* case: H0 => Hr2. *)
-  (* move => A B Heq. *)
-  (* hAndDestruct (Hr1 _ _ Heq) => HAB1 HBA1. *)
-  (* hAndDestruct (Hr2 _ _ Heq) => HAB2 HBA2. *)
-  (* hSplit. *)
-  (* - apply:  *)
-(* Qed. *)
+Instance imp_both_rewriteable(r1 : form -> form)(r2 : form -> form) `{Rewriteable r1} `{Rewriteable r2} : Rewriteable (fun B => r1 B ->> r2 B) := {}.
+Proof.
+  case: H => Hr1.
+  case: H0 => Hr2.
+  move => A B Heq.
+  hAndDestruct (Hr1 _ _ Heq) => HAB1 HBA1.
+  hAndDestruct (Hr2 _ _ Heq) => HAB2 HBA2.
+  hSplit.
+  - apply: gqm_mp; last by apply: HBA1.
+    apply: gqm_mp; first by apply: gqm_swap.
+    apply: gqm_mp; last by apply: HAB2.
+    apply: gqm_3chain.
+  - apply: gqm_mp; last by apply: HAB1.
+    apply: gqm_mp; first by apply: gqm_swap.
+    apply: gqm_mp; last by apply: HBA2.
+    apply: gqm_3chain.
+Qed.
 
 
 Instance box_rewriteable(r : form -> form) `{Rewriteable r} : Rewriteable (fun X => |[]| (r X)) := {}.
@@ -103,14 +127,14 @@ Proof.
   by case: (box_rewriteable ssrfun.id).
 Qed.
 
-(* Instance subst_rewriteable(r : form -> form) `{Rewriteable r} (f: var -> form) : Rewriteable (fun X => subst f (r X)) := {}. *)
-(* Proof. *)
-  (* case: H => Hr. *)
-  (* move => A B Heq. *)
-  (* have H := (Hr _ _ Heq). *)
-  (* have -> : (((r A).[f] <<->> (r B).[f]) = subst f (r A <<->> r B)) by asimpl. *)
-
-(* Qed. *)
+Instance subst_rewriteable(r : form -> form) `{Rewriteable r} (f: var -> form) : Rewriteable (fun X => subst f (r X)) := {}.
+Proof.
+  case: H => Hr.
+  move => A B Heq.
+  have := (Hr _ _ Heq); clear Hr Heq.
+  have -> : (((r A).[f] <<->> (r B).[f]) = subst f (r A <<->> r B)) by asimpl.
+  (* TODO *)
+Abort.
 
 
 (* this is here for testing purposes *)
@@ -175,27 +199,27 @@ Qed.
   (* done. *)
 (* Qed. *)
 
-(* Example rewrite_test_5 : forall A B, |-- (A <<->> B) -> |-- (A <<->> -!-!B). *)
-(* Proof. *)
-  (* move => A B Himp. *)
-  (* have H : (|-- (A <<->> B) <<->> (A <<->> -!-!B)). { *)
-    (* apply (@form_rewrite (fun X => A <<->> X) _ _ _ (gqm_dnegEquiv B)). *)
-  (* } *)
-  (* hAndDestruct H => H _. *)
-  (* apply: gqm_mp; first by apply H. *)
-  (* done. *)
-(* Qed. *)
+Example rewrite_test_5 : forall A B, |-- (A <<->> B) -> |-- (A <<->> -!-!B).
+Proof.
+  move => A B Himp.
+  have H : (|-- (A <<->> B) <<->> (A <<->> -!-!B)). {
+    apply (@form_rewrite (fun X => A <<->> X) _ _ _ (gqm_dnegEquiv B)).
+  }
+  hAndDestruct H => H _.
+  apply: gqm_mp; first by apply H.
+  done.
+Qed.
 
 Lemma tac_rewrite(r: form -> form) `{Rewriteable r} :
-  forall A B, |-- A <<->> B -> |-- r A -> |-- r B.
+  forall A B, |-- A <<->> B -> |-- r B -> |-- r A.
 Proof.
   case: H => Hr.
   move => A B Heq HA.
-  hAndDestruct (Hr _ _ Heq) => HAB _.
+  hAndDestruct (Hr _ _ Heq) => _ HAB.
   by apply: gqm_mp; first by apply HAB.
 Qed.
 
-Example rewrite_test_1' : forall A B, |-- A ->> B -> |-- A ->> -!-!B.
+Example rewrite_test_1' : forall A B, |-- A ->> -!-!B -> |-- A ->> B.
 Proof.
   move => A B Himp.
   by apply: (tac_rewrite (fun X => A ->> X) _ _ (gqm_dnegEquiv B)).
@@ -204,20 +228,26 @@ Qed.
 Tactic Notation "hRewrite" constr(Heq) constr(fShape) :=
   apply: (tac_rewrite fShape _ _ Heq).
 
-Example rewrite_test_2' : forall A B, |-- [A](A ->> B) -> |-- [A](A ->> -!-!B).
+Example rewrite_test_2' : forall A B, |-- [A](A ->> -!-!B) -> |-- [A](A ->> B).
 Proof.
   move => A B Himp.
   by hRewrite (gqm_dnegEquiv B) (fun X => [A](A ->> X)).
 Qed.
 
-Example rewrite_test_3' : forall A B, |-- [A](A ->> [A] B) -> |-- [A](A ->> [A]-!-!B).
+Example rewrite_test_3' : forall A B, |-- [A](A ->> [A] -!-!B) -> |-- [A](A ->> [A]B).
 Proof.
   move => A B Himp.
   by hRewrite (gqm_dnegEquiv B) (fun X => [A](A ->> [A] X)).
 Qed.
 
-Example rewrite_test_4' : forall A B, |-- [A](A ->> [A]|[]| B) -> |-- [A](A ->> [A]|[]|-!-!B).
+Example rewrite_test_4' : forall A B, |-- [A](A ->> [A]|[]| -!-!B) -> |-- [A](A ->> [A]|[]|B).
 Proof.
   move => A B Himp.
   by hRewrite (gqm_dnegEquiv B) (fun X => [A](A ->> [A]|[]| X)).
 Qed.
+
+Example rewrite_test_5' : forall A B, |-- (A <<->> -!-!B) -> |-- (A <<->> B).
+Proof.
+  move => A B Himp.
+  by hRewrite (gqm_dnegEquiv B) (fun X => A <<->> X).
+Qed.
\ No newline at end of file
diff --git a/theories/Section5.v b/theories/Section5.v
index 352dec3e9866f4488b59bee1d2f37e7a60225b45..1a774a4260697f794cfaf3e13ffaa72b4d5ffaff 100644
--- a/theories/Section5.v
+++ b/theories/Section5.v
@@ -38,24 +38,19 @@ Qed.
 Lemma lemma_A_2_3 : forall A, |-- [A]A <<->> -!<E>-!A.
 Proof.
   move => A.
+  hRewrite (gqm_dnegEquiv A) (fun X => [A]X <<->> -!<E>-!A).
+  hAndDestruct (lemma_A_2_1 (-! A)) => H1 H2.
   hSplit.
-  - apply: gqm_mp; first by apply: gqm_contrap3.
-    hRewrite (gqm_dnegEquivR A) (fun X => <E> -! A ->> -! ([A] X)).
-    by hAndDestruct (lemma_A_2_1 (-! A)).
-  - apply: gqm_mp; first by apply: gqm_contrap2.
-    hRewrite (gqm_dnegEquivR A) (fun X => -! ([A] X) ->> <E> -! A).
-    by hAndDestruct (lemma_A_2_1 (-! A)).
+  - by apply: gqm_mp; first by apply: gqm_contrap3.
+  - by apply: gqm_mp; first by apply: gqm_contrap2.
 Qed.
 
 Lemma lemma_A_2_4 : forall A, |-- [E]A <<->> -!<A>-!A.
 Proof.
   move => A.
   hSplit.
-  (* - apply: gqm_mp; first by apply: gqm_contrap3. *)
-    (* Set Typeclasses Debug. *)
-    (* apply (tac_rewrite (fun X => <A> -! A ->> -! ([E] X)) _ _ (gqm_dnegEquivR A)). *)
-    (* hRewrite (gqm_dnegEquivR A) (fun X => <A> -! A ->> -! ([E] X)). *)
-
+  (* TODO: rewrite does not work here *)
+  (* hRewrite (gqm_dnegEquivR A) (fun X => <A> -! A ->> -! ([E] X)). *)
   - apply: gqm_mp.
     + apply: gqm_mp; first by apply: (gqm_chain _ (([E] -! -! A))).
       apply: gqm_mp; first by apply: gqm_contrap3.
@@ -100,7 +95,7 @@ Qed.
 
 (** ** Lemma 5.3 *)
 
-(** *** Lemma A.5 *)
+(** *** Lemma A.4 *)
 Lemma lemma_A_4_1 : forall A B, |-- [A](A.[change_top(B)]) ->> [E]A.
 Proof.
   move => A B.
@@ -112,4 +107,24 @@ Proof.
     apply: gqm_mp; first by apply: gqm_contrap.
     apply: gqm_id.
   - apply: gqm_AE.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma lemma_A_4_2 : forall X Phi A, |-- (X & [A](Phi.[ren (+1)])) ->> A -> |-- (X & [E]Phi) ->> A.
+Proof.
+  move => X Phi A H.
+  have H2 : (|-- (X & -! A) ->> -![A](Phi.[ren (+1)])) by apply: gqm_mp; first by apply: gqm_contrapAndR.
+  Fail have H3 : (|-- (X & -! A) ->> [A](-![A](Phi.[ren (+1)])).[ren(+1)]) by apply: gqm_univgen.
+  (* TODO: fix *)
+Abort.
+
+(** *** Lemma A.5 *)
+Lemma lemma_A_5_1_1 : forall A B, |-- A ->> B -> |-- [A]A ->> [A]B.
+Proof.
+    by apply: lemma_A_1.
+Qed.
+
+Lemma lemma_A_5_1_2 : forall A B, |-- A ->> B -> |-- [E]A ->> [E]B.
+Proof.
+  move => A B Himp.
+  (* TODO*)
+Abort.