lemma 5.6(i)

theories/Section5WithContext.v

@@ -19,13 +19,15 @@ Inductive GQMdedWithContext: list form -> form -> Prop :=
 Notation "c '|--' A"  := (GQMdedWithContext c A) (at level 80, no associativity).
 Hint Constructors GQMdedWithContext : GQMDB.
 
-Fixpoint context_to_form(l : list form) :=
-  match l with
-  | [] => Top
-  | A :: l' => A & context_to_form(l')
-  end.
+Lemma gqmc_context_weakening : forall c A B, c |-- A -> B::c |-- A.
+Proof.
+  move => c A B.
+  by elim; clear c A; eauto using in_cons with GQMDB.
+Qed.
+
+Definition context_to_and := fold_right (fun A B => A & B) Top.
 
-Lemma lemma_5_6_1 : forall c A, c |-- A <-> |-- |A| (context_to_form c) ->> |A|A.
+Lemma lemma_5_6_1 : forall c A, c |-- A <-> |-- |A| (context_to_and c) ->> |A|A.
 Proof.
   move => c A.
   split.
@@ -54,4 +56,22 @@ Proof.
       by apply: lemma_A_7_1.
     + move => _ IH.
         by apply: (tac_rewrite (fun X => _ ->> X) (lemma_A_7_8_1 _)).
-  -
\ No newline at end of file
+  - move => Hgqm.
+    suff H : (c |-- |A|A). {
+      have He := (gqmc_gqm c _ (gqm_AE (A._[ren_ (+1)]) (Var 1))).
+      asimpl in He.
+      by apply: gqmc_mp; first by apply: He.
+    }
+    apply: gqmc_mp; first by apply: (gqmc_gqm c _ Hgqm).
+    clear Hgqm A.
+    apply: gqmc_Anec.
+    elim: c => /=.
+    + apply: gqmc_gqm.
+        by apply: gqm_topI.
+    + move => A l IH.
+      apply: gqmc_mp; last by apply: (gqmc_context_weakening _ _ A IH).
+      clear IH.
+      apply: (gqmc_mp _ A); last by eauto using in_eq with GQMDB.
+      apply: gqmc_gqm.
+        by apply: gqm_andI.
+Qed.
\ No newline at end of file