changed definition of Global_Form to exclude box and proofed missing lemma

theories/GQM.v

@@ -84,7 +84,7 @@ Fixpoint Global_Form(A: form) :=
   match A with
   | Var _ => False
   | Imp f g => Global_Form f /\ Global_Form g
-  | Box f => Global_Form f
+  | Box f => False
   | SquareAll _ => True
   end.
 

theories/Section5WithContext.v

@@ -79,22 +79,36 @@ Qed.
 Lemma lemma_5_6_2_global_all : forall A, Global_Form A -> |-- A <<->> |A| A.
 Proof.
   elim => // /=.
-  (* Focus 2. *)
-  (* - move => f IHf Hf. *)
-    (* hSplit; last by apply: lemma_A_7_4. *)
-    (* have {Hf IHf} Hf := IHf Hf. *)
-    (* apply: gqm_mp; first by apply: lemma_A_7_4. *)
-
   - move => f IHf g IHg [Hf Hg].
     hSplit; last by apply: lemma_A_7_4.
     have {IHf Hf} Hf := IHf Hf.
     have {IHg Hg} Hg := IHg Hg.
     apply: (tac_rewrite (fun X => (X ->> _) ->> |A|(f ->> g)) Hf).
     apply: (tac_rewrite (fun X => (_ ->> X) ->> |A|(f ->> g)) Hg).
-    apply: (tac_rewrite (fun X => (|A| f ->> |A|g) ->> |A|(X ->> g)) Hf).
-    apply: (tac_rewrite (fun X => (|A| f ->> |A|g) ->> |A|(_ ->> X)) Hg).
-    (* TODO *)
-Admitted.
+    apply: gqm_mp.
+    + apply: gqm_mp; first by apply: gqm_negE3 (|A| f) _.
+      apply: gqm_mp; first by apply: gqm_swap.
+      apply: gqm_mp; first by apply: gqm_chain.
+      apply: gqm_mp; first by apply: lemma_A_7_1.
+      apply: gqm_Anec.
+      apply: gqm_subst.
+        by apply: gqm_I1.
+    + apply: gqm_mp; first by apply: gqm_discardr.
+      have Hneg : (|-- -! (|A| f) ->> |A| (-! f)). {
+        apply: gqm_mp; first by apply: gqm_contrap2.
+        apply: (tac_rewrite (fun X => ((-! (|A| -! X)) ->> |A| f)) Hf).
+        by hAndDestruct (lemma_A_7_7 f).
+      }
+      apply: gqm_mp; last by apply: Hneg.
+      apply: gqm_mp; first by apply: gqm_chain.
+      apply: gqm_mp; first by apply: lemma_A_7_1.
+      apply: gqm_Anec.
+      apply: gqm_subst.
+      apply: gqm_mp; first by apply: gqm_chain.
+      by apply: gqm_negE.
+  - move => f _ _.
+    by apply: lemma_A_7_11_1.
+Qed.
 
 
 Lemma lemma_5_6_2 : forall c A,