used new proof of lemma A_4_2

theories/Section5.v

@@ -132,10 +132,36 @@ Proof.
   (* (2) *)
   have H2 : (|-- (X.[ren (+1)] & -! A.[ren (+1)]) ->> -![A](Phi.[ren (+1)])) by apply: gqm_mp; first by apply: gqm_contrapAndR.
   (* (3) *)
-  have H3 := (gqm_Q5 (Phi.[ren (+1)])).
-  Fail have H3 : (|-- (X & -! A) ->> [A](-![A](Phi.[ren (+1)]))) by apply: gqm_univgen.
-  (* TODO: fix *)
-Admitted.
+  have H3 := (gqm_Q5 (Phi._[ren_ (+1)])).
+  (* (4) *)
+  have H4 : (|-- X.[ren (+1)] & -! A.[ren (+1)] ->> [A] (-! ([A] Phi.[ren (+1)])).[ren (+1)]). {
+    apply: gqm_mp; last by apply: H2.
+    by apply: gqm_mp; first by apply: gqm_chain.
+  }
+  (* (5) *)
+  have Hr : ((X.[ren (+1)] & -! A.[ren (+1)]) = (X & -! A).[ren (+1)]) by asimpl.
+  rewrite Hr in H4; clear Hr.
+  have H5 := (gqm_univgen _ _ H4).
+  (* (6) *)
+  have H6 := (gqm_AE ((-! ([A] Phi._[ren_ (+1)]))._[ren_ (+1)]) (Var 0)).
+  asimpl in H6.
+  rewrite !ids_0_neg in H6.
+  (* (7) *)
+  have H7 := (lemma_A_1 _ _ H6).
+  (* (8) *)
+  have H8 : (|-- X & -! A ->> [A] -! ([A] Phi.[ren (+1)])). {
+    apply: gqm_mp; last by apply: H5.
+    apply: gqm_mp; first by apply: gqm_chain.
+    by asimpl.
+  }
+  (* (9) noop *)
+  (* (10) noop *)
+  (* (11) noop *)
+  (* (12) *)
+  rewrite /SquareExists /All /DiamondExists.
+  apply: (tac_rewrite (fun Y => _ ->> Y) (gqm_dnegEquiv _)).
+  by apply: gqm_mp; first by apply: gqm_contrapAndR.
+Qed.
 
 Lemma lemma_A_4_2_simple : forall Phi A, |-- [A](Phi.[ren (+1)]) ->> A.[ren (+1)] -> |-- [E]Phi ->> A.
 Proof.