From 166d5775e0c4a55df2a5e073dba3a088fa7b3012 Mon Sep 17 00:00:00 2001
From: babireski <elian.babireski@gmail.com>
Date: Tue, 15 Apr 2025 14:10:38 -0300
Subject: [PATCH 1/2] Fix context out of section error

---
 coq/Completeness.v        |   3 +-
 coq/Examples.v            | 240 ++++-----
 coq/Frame_Validation.v    | 990 +++++++++++++++++++-------------------
 coq/Logical_Equivalence.v | 200 ++++----
 coq/Makefile              | 122 ++---
 5 files changed, 763 insertions(+), 792 deletions(-)

diff --git a/coq/Completeness.v b/coq/Completeness.v
index 19c1c63..96418ac 100644
--- a/coq/Completeness.v
+++ b/coq/Completeness.v
@@ -2,6 +2,7 @@ Require Import Decidable Equality Relations.
 Require Import Modal_Library Modal_Notations Modal_Tactics Deductive_System Soundness List Classical Bool Sets.
 Set Implicit Arguments.
 
+Section Completeness.
 Context `{X: modal_index_set}.
 
 (* Assume that formulas are constructively countable for now. *)
@@ -151,8 +152,6 @@ Proof.
   - assumption.
 Qed.
 
-Section Completeness.
-
   Variable A: axiom -> Prop.
 
   Hypothesis extending_P: Subset P A.
diff --git a/coq/Examples.v b/coq/Examples.v
index 924a9e1..6be6602 100644
--- a/coq/Examples.v
+++ b/coq/Examples.v
@@ -1,131 +1,133 @@
 Require Import List Modal_Library Modal_Notations Deductive_System Modal_Tactics Sets.
 Import ListNotations.
 
-Context `{X: modal_index_set}.
+Section Examples.
+  Context `{X: modal_index_set}.
 
-Definition fixed_point A G i :=
-  forall f,
-  exists p,
-  (A; G |-- [! (p <-> f ([i] p))!]).
+  Definition fixed_point A G i :=
+    forall f,
+    exists p,
+    (A; G |-- [! (p <-> f ([i] p))!]).
 
-Definition subset {T} (P: T -> Prop) (Q: T -> Prop): Prop :=
-  forall x, P x -> Q x.
+  Definition subset {T} (P: T -> Prop) (Q: T -> Prop): Prop :=
+    forall x, P x -> Q x.
 
-(* Some quick automation! *)
-Local Hint Unfold subset: modal.
-Local Hint Constructors P: modal.
-Local Hint Constructors K: modal.
-Local Hint Constructors K4: modal.
+  (* Some quick automation! *)
+  Local Hint Unfold subset: modal.
+  Local Hint Constructors P: modal.
+  Local Hint Constructors K: modal.
+  Local Hint Constructors K4: modal.
 
-Theorem Lob:
-  (* Löb's theorem is provable in any superset of K4 with fixed points. *)
-  forall A i,
-  subset (K4 i) A /\ fixed_point A Empty i ->
-  forall p,
-  (A; Empty |-- [! [i]p -> p !]) ->
-  (A; Empty |-- [! p !]).
-Proof.
-  set (G := Empty).
-  (* Step 1. *)
-  intros A i [I FP] p H1.
-  (* Step 2. *)
-  destruct FP with (fun X => [! X -> p !]) as (psi, H2).
-  (* Step 3. *)
-  assert (A; G |-- [! psi -> [i]psi -> p !]) as H3.
-  apply modal_ax5 in H2; auto with modal.
-  (* Step 4. *)
-  assert (A; G |-- [! [i](psi -> [i]psi -> p) !]) as H4.
-  apply Nec; auto.
-  (* Step 5. *)
-  assert (A; G |-- [! [i]psi -> [i]([i]psi -> p) !]) as H5.
-  apply modal_axK in H4; auto with modal.
-  (* Step 6. *)
-  assert (A; G |-- [! [i]([i]psi -> p) -> [i][i]psi -> [i]p !]) as H6.
-  eapply Ax with (a := axK i ?[X] ?[Y]); auto with modal.
-  reflexivity.
-  (* Step 7. *)
-  assert (A; G |-- [! [i]psi -> [i][i]psi -> [i]p !]) as H7.
-  eapply modal_syllogism; eauto with modal.
-  (* Step 8. *)
-  assert (A; G |-- [! [i]psi -> [i][i]psi !]) as H8.
-  apply modal_axK4; auto with modal.
-  (* Step 9. *)
-  assert (A; G |-- [! [i]psi -> [i]p !]) as H9.
-  eapply modal_ax2; eauto with modal.
-  (* Step 10. *)
-  assert (A; G |-- [! [i]psi -> p !]) as H10.
-  eapply modal_syllogism; eauto with modal.
-  (* Step 11. *)
-  assert (A; G |-- [! ([i]psi -> p) -> psi !]) as H11.
-  apply modal_ax6 in H2; auto with modal.
-  (* Step 12. *)
-  assert (A; G |-- psi) as H12.
-  eapply Mp; try eassumption.
-  (* Step 13. *)
-  assert (A; G |-- [! [i]psi !]) as H13.
-  apply Nec; try assumption.
-  (* Step 14. *)
-  eapply Mp; eassumption.
-Qed.
+  Theorem Lob:
+    (* Löb's theorem is provable in any superset of K4 with fixed points. *)
+    forall A i,
+    subset (K4 i) A /\ fixed_point A Empty i ->
+    forall p,
+    (A; Empty |-- [! [i]p -> p !]) ->
+    (A; Empty |-- [! p !]).
+  Proof.
+    set (G := Empty).
+    (* Step 1. *)
+    intros A i [I FP] p H1.
+    (* Step 2. *)
+    destruct FP with (fun X => [! X -> p !]) as (psi, H2).
+    (* Step 3. *)
+    assert (A; G |-- [! psi -> [i]psi -> p !]) as H3.
+    apply modal_ax5 in H2; auto with modal.
+    (* Step 4. *)
+    assert (A; G |-- [! [i](psi -> [i]psi -> p) !]) as H4.
+    apply Nec; auto.
+    (* Step 5. *)
+    assert (A; G |-- [! [i]psi -> [i]([i]psi -> p) !]) as H5.
+    apply modal_axK in H4; auto with modal.
+    (* Step 6. *)
+    assert (A; G |-- [! [i]([i]psi -> p) -> [i][i]psi -> [i]p !]) as H6.
+    eapply Ax with (a := axK i ?[X] ?[Y]); auto with modal.
+    reflexivity.
+    (* Step 7. *)
+    assert (A; G |-- [! [i]psi -> [i][i]psi -> [i]p !]) as H7.
+    eapply modal_syllogism; eauto with modal.
+    (* Step 8. *)
+    assert (A; G |-- [! [i]psi -> [i][i]psi !]) as H8.
+    apply modal_axK4; auto with modal.
+    (* Step 9. *)
+    assert (A; G |-- [! [i]psi -> [i]p !]) as H9.
+    eapply modal_ax2; eauto with modal.
+    (* Step 10. *)
+    assert (A; G |-- [! [i]psi -> p !]) as H10.
+    eapply modal_syllogism; eauto with modal.
+    (* Step 11. *)
+    assert (A; G |-- [! ([i]psi -> p) -> psi !]) as H11.
+    apply modal_ax6 in H2; auto with modal.
+    (* Step 12. *)
+    assert (A; G |-- psi) as H12.
+    eapply Mp; try eassumption.
+    (* Step 13. *)
+    assert (A; G |-- [! [i]psi !]) as H13.
+    apply Nec; try assumption.
+    (* Step 14. *)
+    eapply Mp; eassumption.
+  Qed.
 
-(* TODO: review later!
+  (* TODO: review later!
 
-Definition fromList (ps: list formula): theory :=
-  fun p =>
-    In p ps.
+  Definition fromList (ps: list formula): theory :=
+    fun p =>
+      In p ps.
 
-Example Ex1:
-  (* TODO: fix notation for deduction! *)
-  T; (fromList ([! [](#0 -> #1) !] :: [! [](#1 -> #2) !] :: nil)) |--
-    [! [](#0 -> #2) !].
-Proof.
-  (* Line: 16 *)
-  apply Nec.
-  (* Line: 15 *)
-  apply Mp with (f := [! #0 -> #1 !]).
-    (* Line: 14 *)
-  - apply Mp with (f := [! #1 -> #2 !]).
-      (* Line: 9 *)
-    + apply Mp with (f := [! (#1 -> #2) -> (#0 -> (#1 -> #2)) !]).
-        (* Line: 7 *)
-      * apply Mp with (f := [! (#1 -> #2) -> ((#0 -> (#1 -> #2)) -> (#0 -> #1) -> (#0 -> #2)) !]).
-          (* Line: 6 *)
-        -- apply Ax with (a := ax2 [! #1 -> #2 !] [! #0 -> (#1 -> #2) !] [! (#0 -> #1) -> (#0 -> #2) !]).
-          ++ constructor.
-             constructor.
-          ++ reflexivity.
-        (* Line: 5 *)
-        -- apply Mp with (f := [! (#0 -> (#1 -> #2)) -> ((#0 -> #1) -> (#0 -> #2)) !]).
-          (* Line: 3 *)
-          ++ apply Ax with (a := ax1 [! (#0 -> (#1 -> #2)) -> ((#0 -> #1) -> (#0 -> #2)) !] [! #1 -> #2 !]).
-            ** constructor.
-               constructor.
-            ** reflexivity.
-          (* Line: 4 *)
-          ++ apply Ax with (a := ax2 [! #0 !] [! #1 !] [! #2 !]).
-            ** constructor; constructor.
-            ** reflexivity.
-        (* Line: 8 *)
-      * apply Ax with (a := ax1 [! #1 -> #2 !] [! #0 !]).
-        -- constructor; constructor.
-        -- reflexivity.
-      (* Line: 11 *)
-    + apply Mp with (f := [! [](#1 -> #2) !]).
-      * apply Ax with (a := axT [! #1 -> #2 !]).
-        -- constructor; constructor.
-        -- reflexivity.
-        (* Line: 2 *)
-      * apply Prem; simpl.
+  Example Ex1:
+    (* TODO: fix notation for deduction! *)
+    T; (fromList ([! [](#0 -> #1) !] :: [! [](#1 -> #2) !] :: nil)) |--
+      [! [](#0 -> #2) !].
+  Proof.
+    (* Line: 16 *)
+    apply Nec.
+    (* Line: 15 *)
+    apply Mp with (f := [! #0 -> #1 !]).
+      (* Line: 14 *)
+    - apply Mp with (f := [! #1 -> #2 !]).
+        (* Line: 9 *)
+      + apply Mp with (f := [! (#1 -> #2) -> (#0 -> (#1 -> #2)) !]).
+          (* Line: 7 *)
+        * apply Mp with (f := [! (#1 -> #2) -> ((#0 -> (#1 -> #2)) -> (#0 -> #1) -> (#0 -> #2)) !]).
+            (* Line: 6 *)
+          -- apply Ax with (a := ax2 [! #1 -> #2 !] [! #0 -> (#1 -> #2) !] [! (#0 -> #1) -> (#0 -> #2) !]).
+            ++ constructor.
+              constructor.
+            ++ reflexivity.
+          (* Line: 5 *)
+          -- apply Mp with (f := [! (#0 -> (#1 -> #2)) -> ((#0 -> #1) -> (#0 -> #2)) !]).
+            (* Line: 3 *)
+            ++ apply Ax with (a := ax1 [! (#0 -> (#1 -> #2)) -> ((#0 -> #1) -> (#0 -> #2)) !] [! #1 -> #2 !]).
+              ** constructor.
+                constructor.
+              ** reflexivity.
+            (* Line: 4 *)
+            ++ apply Ax with (a := ax2 [! #0 !] [! #1 !] [! #2 !]).
+              ** constructor; constructor.
+              ** reflexivity.
+          (* Line: 8 *)
+        * apply Ax with (a := ax1 [! #1 -> #2 !] [! #0 !]).
+          -- constructor; constructor.
+          -- reflexivity.
+        (* Line: 11 *)
+      + apply Mp with (f := [! [](#1 -> #2) !]).
+        * apply Ax with (a := axT [! #1 -> #2 !]).
+          -- constructor; constructor.
+          -- reflexivity.
+          (* Line: 2 *)
+        * apply Prem; simpl.
+          firstorder.
+      (* Line: 13 *)
+    - apply Mp with (f := [! [](#0 -> #1) !]).
+        (* Line: 12 *)
+      + apply Ax with (a := axT [! #0 -> #1 !]).
+        * constructor; constructor.
+        * reflexivity.
+        (* Line: 1 *)
+      + apply Prem; simpl.
         firstorder.
-    (* Line: 13 *)
-  - apply Mp with (f := [! [](#0 -> #1) !]).
-      (* Line: 12 *)
-    + apply Ax with (a := axT [! #0 -> #1 !]).
-      * constructor; constructor.
-      * reflexivity.
-      (* Line: 1 *)
-    + apply Prem; simpl.
-      firstorder.
-Qed.
+  Qed.
 
-*)
+  *)
+End Examples.
\ No newline at end of file
diff --git a/coq/Frame_Validation.v b/coq/Frame_Validation.v
index a76a454..435ef70 100644
--- a/coq/Frame_Validation.v
+++ b/coq/Frame_Validation.v
@@ -2,505 +2,507 @@ Require Import Decidable.
 Require Import Classical.
 Require Import Modal_Library Modal_Notations Modal_Tactics Classical.
 
-Context `{X: modal_index_set}.
-
-Theorem reflexive_frame_implies_axiomT:
-  forall f p idx,
-  reflexive_frame f idx ->
-  forall v,
-  [f -- v] |= [! [idx]p -> p !].
-Proof.
-  intros f p idx HR v w1 H1.
-  simpl in H1.
-  unfold reflexive_frame in HR.
-  apply H1 in HR.
-  assumption.
-Qed.
-
-Theorem axiomT_implies_reflexive_frame:
-  forall f idx,
-  (forall v p, [f -- v] |= [! [idx]p -> p !]) ->
-  reflexive_frame f idx.
-Proof.
-  intros f idx.
-  apply contrapositive.
-  - apply classic.
-  - intros H; unfold reflexive_frame in H.
-    apply not_all_ex_not in H; destruct H as [w1].
-    apply ex_not_not_all.
-    exists (fun _ x => R f idx w1 x).
-    apply ex_not_not_all.
-    exists [! #0 !].
-    intros H1; unfold validate_model in H1; simpl in H1.
-    destruct H.
-    apply H1.
-    intros w2 H'; assumption.
-Qed.
-
-Theorem transitive_frame_implies_axiom4:
-  forall f idx,
-  transitive_frame f idx ->
-  forall v p,
-  [f -- v] |= [! [idx]p -> [idx][idx]p !].
-Proof.
-  intros f idx H v p w1 H1.
-  simpl.
-  intros w2 H2 w3 H3.
-  simpl in H1.
-  apply H1.
-  unfold transitive_frame in H.
-  apply H with (w := w1) (w' := w2) (w'' := w3).
-  split; assumption.
-Qed.
-
-Theorem axiom4_implies_transitive_frame:
-  forall f idx,
-  (forall v p, [f -- v] |= [! [idx]p -> [idx][idx]p !]) ->
-  transitive_frame f idx.
-Proof.
-  intros f idx.
-  apply contrapositive.
-  - apply classic.
-  - intros H; unfold transitive_frame in H.
-    apply not_all_ex_not in H; destruct H as [w1];
-    apply not_all_ex_not in H; destruct H as [w2];
-    apply not_all_ex_not in H; destruct H as [w3].
-    apply imply_to_and with (P:= R f idx w1 w2 /\ R f idx w2 w3) in H.
-    destruct H as [H1 H3]; destruct H1 as [H1 H2].
-    apply ex_not_not_all.
-    exists (fun _ x => R f idx w1 x).
-    apply ex_not_not_all.
-    exists [! #0 !].
-    intros H; unfold validate_model in H; simpl in H.
-    destruct H3.
-    eapply H.
-    + intros H3 H4; apply H4.
-    + apply H1.
-    + apply H2.
-Qed.
-
-Theorem symmetric_frame_implies_axiomB:
-  forall f idx,
-  symmetric_frame f idx ->
-  forall v p,
-  [f -- v] |= [! p -> [idx]<idx>p !].
-Proof.
-  intros f idx H v p w1 H1.
-  simpl.
-  intros w2 H2.
-  exists w1.
-  unfold symmetric_frame in H.
-  - apply H.
-    assumption.
-  - assumption.
-Qed.
-
-Theorem axiomB_implies_symmetric_frame:
-  forall f idx,
-  (forall v p, [f -- v] |= [! p -> [idx]<idx>p !]) ->
-  symmetric_frame f idx.
-Proof.
-  intros f idx.
-  apply contrapositive.
-  - apply classic.
-  - intros H; unfold symmetric_frame in H.
-    apply not_all_ex_not in H; destruct H as [w1];
-    apply not_all_ex_not in H; destruct H as [w2].
-    apply imply_to_and in H; destruct H as [H1 H2].
-    apply ex_not_not_all.
-    exists (fun _ x => ~ R f idx w2 x).
-    apply ex_not_not_all.
-    exists [! #0 !].
-    intros H; unfold validate_model in H; simpl in H.
-    pose H1 as H3.
-    apply H in H3; try assumption.
-    destruct H3 as [w3].
-    contradiction.
-Qed.
-
-Theorem euclidean_frame_implies_axiom5:
-  forall f idx,
-  euclidian_frame f idx ->
-  forall v p,
-  [f -- v] |= [! <idx>p -> [idx]<idx>p !].
-Proof.
-  intros f idx H v p w1 H1.
-  simpl.
-  intros w2 H2.
-  unfold euclidian_frame in H.
-  destruct H1 as (w3, ?, ?).
-  exists w3.
-  - apply H with w1.
-    firstorder.
-  - assumption.
-Qed.
-
-Theorem axiom5_implies_euclidean_frame:
-  forall f idx,
-  (forall v p, [f -- v] |= [! <idx>p -> [idx]<idx>p !]) ->
-  euclidian_frame f idx.
-Proof.
-  intros f idx.
-  apply contrapositive.
-  - apply classic.
-  - intros H; unfold euclidian_frame in H.
-    apply not_all_ex_not in H; destruct H as [w1];
-    apply not_all_ex_not in H; destruct H as [w2];
-    apply not_all_ex_not in H; destruct H as [w3].
-    apply imply_to_and with (P := R f idx w1 w2 /\ R f idx w1 w3) in H.
-    destruct H as [H1 H3]; destruct H1 as [H1 H2].
-    apply ex_not_not_all.
-    exists (fun _ x =>  ~ R f idx w2 x).
-    apply ex_not_not_all.
-    exists [! #0 !].
-    intros H; unfold validate_model in H; simpl in H.
-    destruct H with (w1) (w2); try assumption.
-    + exists w3; assumption.
-    + contradiction.
-Qed.
-
-Theorem serial_frame_implies_axiomD:
-  forall f idx,
-  serial_frame f idx ->
-  forall v p,
-  [f -- v] |= [! [idx]p -> <idx>p !].
-Proof.
-  intros f idx H v p w1 H1.
-  unfold serial_frame in H.
-  destruct H with (w1) as [w2].
-  simpl in *.
-  exists w2.
-  - assumption.
-  - apply H1.
+Section Validation.
+  Context `{X: modal_index_set}.
+
+  Theorem reflexive_frame_implies_axiomT:
+    forall f p idx,
+    reflexive_frame f idx ->
+    forall v,
+    [f -- v] |= [! [idx]p -> p !].
+  Proof.
+    intros f p idx HR v w1 H1.
+    simpl in H1.
+    unfold reflexive_frame in HR.
+    apply H1 in HR.
     assumption.
-Qed.
-
-Theorem axiomD_implies_serial_frame: 
-  forall f idx,
-  (forall v p, [f -- v] |= [! [idx]p -> <idx>p !]) ->
-  serial_frame f idx.
-Proof.
-  intros f idx.
-  apply contrapositive.
-  - apply classic.
-  - intros H.
-    unfold serial_frame in H.
-    apply not_all_ex_not in H; destruct H as [w1].
-    apply ex_not_not_all.
-    exists (fun _ x => ~ R f idx w1 x).
-    apply ex_not_not_all.
-    exists [! #0 !].
-    intros H1; unfold validate_model in H1; simpl in H1.
-    edestruct H1.
-    + intros w2 H2.
+  Qed.
+
+  Theorem axiomT_implies_reflexive_frame:
+    forall f idx,
+    (forall v p, [f -- v] |= [! [idx]p -> p !]) ->
+    reflexive_frame f idx.
+  Proof.
+    intros f idx.
+    apply contrapositive.
+    - apply classic.
+    - intros H; unfold reflexive_frame in H.
+      apply not_all_ex_not in H; destruct H as [w1].
+      apply ex_not_not_all.
+      exists (fun _ x => R f idx w1 x).
+      apply ex_not_not_all.
+      exists [! #0 !].
+      intros H1; unfold validate_model in H1; simpl in H1.
       destruct H.
-      exists w2; exact H2.
-    + contradiction.
-Qed.
-
-Theorem functional_frame_implies_axiom:
-  forall f idx,
-  functional_frame f idx ->
-  forall v p,
-  [f -- v] |= [! <idx>p -> [idx]p !].
-Proof.
-  intros f idx H v p w1 H1 w2 H2.
-  unfold functional_frame in H.
-  simpl in H1.
-  destruct H1 as [w3 H1].
-  assert (H4: R f idx w1 w2 /\ R f idx w1 w3) by firstorder.
-  apply H in H4; subst; assumption.
-Qed.
-
-Theorem axiom_implies_functional_frame:
-  forall f idx,
-  (forall v p, [f -- v] |= [! <idx>p -> [idx]p !]) ->
-  functional_frame f idx.
-Proof.
-  intros f idx.
-  apply contrapositive.
-  - apply classic.
-  - intros H; unfold functional_frame in H.
-    apply not_all_ex_not in H; destruct H as [w1];
-    apply not_all_ex_not in H; destruct H as [w2];
-    apply not_all_ex_not in H; destruct H as [w3].
-    apply imply_to_and with (P := R f idx w1 w2 /\ R f idx w1 w3) in H.
-    destruct H as [H1 H3]; destruct H1 as [H1 H2].
-    apply ex_not_not_all.
-    exists (fun _ x => R f idx w1 x /\ x <> w3).
-    apply ex_not_not_all.
-    exists [! #0 !].
-    intros H; unfold validate_model in H; simpl in H.
-    apply H in H2.
-    + destruct H2 as [H2 H4]; contradiction.
-    + exists w2; repeat split; assumption.
-Qed.
-
-Theorem dense_frame_implies_axiom:
-  forall f idx,
-  dense_frame f idx ->
-  forall v p,
-  [f -- v] |= [! [idx][idx]p -> [idx]p !].
-Proof.
-  intros f idx H v p w1 H1 w2 H2.
-  unfold dense_frame in H.
-  destruct H with (w1) (w2) as [w3].
-  simpl in H1.
-  apply H0 in H2; destruct H2 as [H2 H3].
-  apply H1 with (w3); assumption.
-Qed.
-
-Theorem axiom_implies_dense_frame:
-  forall f idx,
-  (forall v p, [f -- v] |= [! [idx][idx]p -> [idx]p !]) ->
-  dense_frame f idx.
-Proof.
-  intros f idx.
-  apply contrapositive.
-  - apply classic.
-  - intros H; unfold dense_frame in H.
-    apply not_all_ex_not in H; destruct H as [w1];
-    apply not_all_ex_not in H; destruct H as [w2].
-    apply ex_not_not_all.
-    exists (fun _ x => exists y, R f idx w1 y /\ R f idx y x).
-    apply ex_not_not_all.
-    exists [! #0 !].
-    intros H1; unfold validate_model in H1; simpl in H1. 
-    edestruct H1.
-    + intros w3 H3 w4 H4.
-      exists w3; split; [apply H3 | assumption].
-    + eapply not_ex_all_not in H.
-      apply imply_to_and in H; destruct H as [H H']; exact H.
-    + eapply not_ex_all_not in H.
-      apply imply_to_and in H; destruct H as [H H']; apply not_and_or in H'.
-      destruct H0 as [H2 H3].
-      Unshelve.
-      destruct H' as [H' | H''].
-      * apply H' in H2; contradiction.
-      * apply H'' in H3; contradiction.
-      * assumption.
-Qed.
-
-Theorem convergent_frame_implies_axiom:
-  forall f idx,
-  convergent_frame f idx ->
-  forall v p,
-  [f -- v] |= [! <idx>[idx]p -> [idx]<idx> p !].
-Proof.
-  intros f idx H v p w1 H1 w2 H2.
-  unfold convergent_frame in H.
-  destruct H1 as (w3, ?, ?).
-  destruct H with w1 w2 w3 as (w4, (?, ?)).
-  - firstorder.
-  - exists w4.
-    + assumption.
-    + apply H1.
+      apply H1.
+      intros w2 H'; assumption.
+  Qed.
+
+  Theorem transitive_frame_implies_axiom4:
+    forall f idx,
+    transitive_frame f idx ->
+    forall v p,
+    [f -- v] |= [! [idx]p -> [idx][idx]p !].
+  Proof.
+    intros f idx H v p w1 H1.
+    simpl.
+    intros w2 H2 w3 H3.
+    simpl in H1.
+    apply H1.
+    unfold transitive_frame in H.
+    apply H with (w := w1) (w' := w2) (w'' := w3).
+    split; assumption.
+  Qed.
+
+  Theorem axiom4_implies_transitive_frame:
+    forall f idx,
+    (forall v p, [f -- v] |= [! [idx]p -> [idx][idx]p !]) ->
+    transitive_frame f idx.
+  Proof.
+    intros f idx.
+    apply contrapositive.
+    - apply classic.
+    - intros H; unfold transitive_frame in H.
+      apply not_all_ex_not in H; destruct H as [w1];
+      apply not_all_ex_not in H; destruct H as [w2];
+      apply not_all_ex_not in H; destruct H as [w3].
+      apply imply_to_and with (P:= R f idx w1 w2 /\ R f idx w2 w3) in H.
+      destruct H as [H1 H3]; destruct H1 as [H1 H2].
+      apply ex_not_not_all.
+      exists (fun _ x => R f idx w1 x).
+      apply ex_not_not_all.
+      exists [! #0 !].
+      intros H; unfold validate_model in H; simpl in H.
+      destruct H3.
+      eapply H.
+      + intros H3 H4; apply H4.
+      + apply H1.
+      + apply H2.
+  Qed.
+
+  Theorem symmetric_frame_implies_axiomB:
+    forall f idx,
+    symmetric_frame f idx ->
+    forall v p,
+    [f -- v] |= [! p -> [idx]<idx>p !].
+  Proof.
+    intros f idx H v p w1 H1.
+    simpl.
+    intros w2 H2.
+    exists w1.
+    unfold symmetric_frame in H.
+    - apply H.
       assumption.
-Qed.
-
-Theorem axiom_implies_convergent_frame:
-  forall f idx,
-  (forall v p, [f -- v] |= [! <idx>[idx]p -> [idx]<idx> p !]) ->
-  convergent_frame f idx.
-Proof.
-  intros f idx.
-  apply contrapositive.
-  - apply classic.
-  - intros H; unfold convergent_frame in H.
-    apply not_all_ex_not in H; destruct H as [w1];
-    apply not_all_ex_not in H; destruct H as [w2];
-    apply not_all_ex_not in H; destruct H as [w3].
-    apply ex_not_not_all.
-    exists (fun _ x => ~ R f idx w3 x).
-    apply ex_not_not_all.
-    exists [! #0 !].
-    intros H5; unfold validate_model in H5; simpl in H5.
-    destruct H5 with w1 w3.
-    + simpl; exists w2.
-      * apply not_ex_all_not with (n := w1) in H.
-        apply imply_to_and in H.
-        destruct H as [H1 H'].
-        destruct H1 as [H1 H2].
+    - assumption.
+  Qed.
+
+  Theorem axiomB_implies_symmetric_frame:
+    forall f idx,
+    (forall v p, [f -- v] |= [! p -> [idx]<idx>p !]) ->
+    symmetric_frame f idx.
+  Proof.
+    intros f idx.
+    apply contrapositive.
+    - apply classic.
+    - intros H; unfold symmetric_frame in H.
+      apply not_all_ex_not in H; destruct H as [w1];
+      apply not_all_ex_not in H; destruct H as [w2].
+      apply imply_to_and in H; destruct H as [H1 H2].
+      apply ex_not_not_all.
+      exists (fun _ x => ~ R f idx w2 x).
+      apply ex_not_not_all.
+      exists [! #0 !].
+      intros H; unfold validate_model in H; simpl in H.
+      pose H1 as H3.
+      apply H in H3; try assumption.
+      destruct H3 as [w3].
+      contradiction.
+  Qed.
+
+  Theorem euclidean_frame_implies_axiom5:
+    forall f idx,
+    euclidian_frame f idx ->
+    forall v p,
+    [f -- v] |= [! <idx>p -> [idx]<idx>p !].
+  Proof.
+    intros f idx H v p w1 H1.
+    simpl.
+    intros w2 H2.
+    unfold euclidian_frame in H.
+    destruct H1 as (w3, ?, ?).
+    exists w3.
+    - apply H with w1.
+      firstorder.
+    - assumption.
+  Qed.
+
+  Theorem axiom5_implies_euclidean_frame:
+    forall f idx,
+    (forall v p, [f -- v] |= [! <idx>p -> [idx]<idx>p !]) ->
+    euclidian_frame f idx.
+  Proof.
+    intros f idx.
+    apply contrapositive.
+    - apply classic.
+    - intros H; unfold euclidian_frame in H.
+      apply not_all_ex_not in H; destruct H as [w1];
+      apply not_all_ex_not in H; destruct H as [w2];
+      apply not_all_ex_not in H; destruct H as [w3].
+      apply imply_to_and with (P := R f idx w1 w2 /\ R f idx w1 w3) in H.
+      destruct H as [H1 H3]; destruct H1 as [H1 H2].
+      apply ex_not_not_all.
+      exists (fun _ x =>  ~ R f idx w2 x).
+      apply ex_not_not_all.
+      exists [! #0 !].
+      intros H; unfold validate_model in H; simpl in H.
+      destruct H with (w1) (w2); try assumption.
+      + exists w3; assumption.
+      + contradiction.
+  Qed.
+
+  Theorem serial_frame_implies_axiomD:
+    forall f idx,
+    serial_frame f idx ->
+    forall v p,
+    [f -- v] |= [! [idx]p -> <idx>p !].
+  Proof.
+    intros f idx H v p w1 H1.
+    unfold serial_frame in H.
+    destruct H with (w1) as [w2].
+    simpl in *.
+    exists w2.
+    - assumption.
+    - apply H1.
+      assumption.
+  Qed.
+
+  Theorem axiomD_implies_serial_frame: 
+    forall f idx,
+    (forall v p, [f -- v] |= [! [idx]p -> <idx>p !]) ->
+    serial_frame f idx.
+  Proof.
+    intros f idx.
+    apply contrapositive.
+    - apply classic.
+    - intros H.
+      unfold serial_frame in H.
+      apply not_all_ex_not in H; destruct H as [w1].
+      apply ex_not_not_all.
+      exists (fun _ x => ~ R f idx w1 x).
+      apply ex_not_not_all.
+      exists [! #0 !].
+      intros H1; unfold validate_model in H1; simpl in H1.
+      edestruct H1.
+      + intros w2 H2.
+        destruct H.
+        exists w2; exact H2.
+      + contradiction.
+  Qed.
+
+  Theorem functional_frame_implies_axiom:
+    forall f idx,
+    functional_frame f idx ->
+    forall v p,
+    [f -- v] |= [! <idx>p -> [idx]p !].
+  Proof.
+    intros f idx H v p w1 H1 w2 H2.
+    unfold functional_frame in H.
+    simpl in H1.
+    destruct H1 as [w3 H1].
+    assert (H4: R f idx w1 w2 /\ R f idx w1 w3) by firstorder.
+    apply H in H4; subst; assumption.
+  Qed.
+
+  Theorem axiom_implies_functional_frame:
+    forall f idx,
+    (forall v p, [f -- v] |= [! <idx>p -> [idx]p !]) ->
+    functional_frame f idx.
+  Proof.
+    intros f idx.
+    apply contrapositive.
+    - apply classic.
+    - intros H; unfold functional_frame in H.
+      apply not_all_ex_not in H; destruct H as [w1];
+      apply not_all_ex_not in H; destruct H as [w2];
+      apply not_all_ex_not in H; destruct H as [w3].
+      apply imply_to_and with (P := R f idx w1 w2 /\ R f idx w1 w3) in H.
+      destruct H as [H1 H3]; destruct H1 as [H1 H2].
+      apply ex_not_not_all.
+      exists (fun _ x => R f idx w1 x /\ x <> w3).
+      apply ex_not_not_all.
+      exists [! #0 !].
+      intros H; unfold validate_model in H; simpl in H.
+      apply H in H2.
+      + destruct H2 as [H2 H4]; contradiction.
+      + exists w2; repeat split; assumption.
+  Qed.
+
+  Theorem dense_frame_implies_axiom:
+    forall f idx,
+    dense_frame f idx ->
+    forall v p,
+    [f -- v] |= [! [idx][idx]p -> [idx]p !].
+  Proof.
+    intros f idx H v p w1 H1 w2 H2.
+    unfold dense_frame in H.
+    destruct H with (w1) (w2) as [w3].
+    simpl in H1.
+    apply H0 in H2; destruct H2 as [H2 H3].
+    apply H1 with (w3); assumption.
+  Qed.
+
+  Theorem axiom_implies_dense_frame:
+    forall f idx,
+    (forall v p, [f -- v] |= [! [idx][idx]p -> [idx]p !]) ->
+    dense_frame f idx.
+  Proof.
+    intros f idx.
+    apply contrapositive.
+    - apply classic.
+    - intros H; unfold dense_frame in H.
+      apply not_all_ex_not in H; destruct H as [w1];
+      apply not_all_ex_not in H; destruct H as [w2].
+      apply ex_not_not_all.
+      exists (fun _ x => exists y, R f idx w1 y /\ R f idx y x).
+      apply ex_not_not_all.
+      exists [! #0 !].
+      intros H1; unfold validate_model in H1; simpl in H1. 
+      edestruct H1.
+      + intros w3 H3 w4 H4.
+        exists w3; split; [apply H3 | assumption].
+      + eapply not_ex_all_not in H.
+        apply imply_to_and in H; destruct H as [H H']; exact H.
+      + eapply not_ex_all_not in H.
+        apply imply_to_and in H; destruct H as [H H']; apply not_and_or in H'.
+        destruct H0 as [H2 H3].
+        Unshelve.
+        destruct H' as [H' | H''].
+        * apply H' in H2; contradiction.
+        * apply H'' in H3; contradiction.
+        * assumption.
+  Qed.
+
+  Theorem convergent_frame_implies_axiom:
+    forall f idx,
+    convergent_frame f idx ->
+    forall v p,
+    [f -- v] |= [! <idx>[idx]p -> [idx]<idx> p !].
+  Proof.
+    intros f idx H v p w1 H1 w2 H2.
+    unfold convergent_frame in H.
+    destruct H1 as (w3, ?, ?).
+    destruct H with w1 w2 w3 as (w4, (?, ?)).
+    - firstorder.
+    - exists w4.
+      + assumption.
+      + apply H1.
         assumption.
-      * intros w4 H4.
-        apply not_ex_all_not with (n := w4) in H.
+  Qed.
+
+  Theorem axiom_implies_convergent_frame:
+    forall f idx,
+    (forall v p, [f -- v] |= [! <idx>[idx]p -> [idx]<idx> p !]) ->
+    convergent_frame f idx.
+  Proof.
+    intros f idx.
+    apply contrapositive.
+    - apply classic.
+    - intros H; unfold convergent_frame in H.
+      apply not_all_ex_not in H; destruct H as [w1];
+      apply not_all_ex_not in H; destruct H as [w2];
+      apply not_all_ex_not in H; destruct H as [w3].
+      apply ex_not_not_all.
+      exists (fun _ x => ~ R f idx w3 x).
+      apply ex_not_not_all.
+      exists [! #0 !].
+      intros H5; unfold validate_model in H5; simpl in H5.
+      destruct H5 with w1 w3.
+      + simpl; exists w2.
+        * apply not_ex_all_not with (n := w1) in H.
+          apply imply_to_and in H.
+          destruct H as [H1 H'].
+          destruct H1 as [H1 H2].
+          assumption.
+        * intros w4 H4.
+          apply not_ex_all_not with (n := w4) in H.
+          apply imply_to_and in H.
+          destruct H as [H1 H'].
+          destruct H1 as [H1 H2].
+          apply not_and_or in H'.
+          firstorder.
+      + apply not_ex_all_not with (n := w1) in H.
         apply imply_to_and in H.
         destruct H as [H1 H'].
         destruct H1 as [H1 H2].
-        apply not_and_or in H'.
-        firstorder.
-    + apply not_ex_all_not with (n := w1) in H.
-      apply imply_to_and in H.
-      destruct H as [H1 H'].
-      destruct H1 as [H1 H2].
-      assumption.
-    + rename x into w4.
-      contradiction.
-Qed.
-
-Theorem modal_double_neg: 
-  forall M w p, (M ' w ||- [! ~~ p !]) -> (M ' w ||- p).
-Proof.
-  intros M w p H; simpl in H; apply NNPP; apply H.
-Qed.
-
-Theorem modal_contra: 
-  forall M p q,
-  (M |= [! ~ p -> ~ q !]) -> (M |= [! q -> p !]).
-Proof.
-  intros M p q H w1 H1.
-  unfold validate_model in H; simpl in *.
-  apply modal_double_neg; intros H2.
-  apply H in H2; contradiction.
-Qed.
-
-Theorem noetherian_frame_implies_axiomGL:
-  forall f idx,
-  noetherian_frame f idx ->
-  forall v p,
-  [f -- v] |= [! [idx]([idx]p -> p) -> [idx]p !].
-Proof.
-  intros f idx H v p.
-  apply modal_contra.
-  intros w H1; simpl in w, H1.
-  apply not_all_ex_not in H1; destruct H1 as [w1 H1];
-  apply imply_to_and in H1; destruct H1 as [H1 H2].
-  set (S := fun w1 => R f idx w w1 /\ ([f -- v] ' w1 ||- [! ~ p !])).
-  destruct H as [H H'];
-  destruct H' with S as [w2 [[H3 H4] H5]]; try (exists w1; split; trivial).
-  clear H'; unfold S in H5; clear S.
-  simpl; apply ex_not_not_all.
-  exists w2.
-  intros H6; simpl in H6.
-  apply H6 in H3; try eauto.
-  intros w3 H7.
-  assert (H8: [f-- v] ' w2 ||- [! [idx] p -> p !]) by (intros ?H; apply H6; assumption);
-  assert (H9: [f-- v] ' w2 ||- [! ~ [idx] p !]) by (intros H9; apply H8 in H9; contradiction).
-  simpl in H9; apply not_all_ex_not in H9;
-  destruct H9 as [w4 H9];
-  apply imply_to_and in H9.
-  assert (H10: (R f idx w2 w4 /\ ~([f--v] ' w4 ||- p)) -> (R f idx w2 w4 /\ ([f--v] ' w4 ||- [! ~ p !]))) by (easy);
-  apply H10 in H9; clear H10.
-  assert (H10: R f idx w w4) by (apply H with (w:=w) (w':=w2) (w'':=w4); easy).
-  destruct H9;
-  assert (H11: R f idx w w4 /\ ([f--v] ' w4 ||- [! ~ p !])) by (easy).
-  apply H5 in H11;
-  contradiction.
-Qed.
-
-(* Proof adapted from: https://planetmath.org/modallogicgl *)
-Lemma GL_implies_4:
-  forall M idx,
-  (forall q, M |= [! [idx]([idx]q -> q) -> [idx]q !]) ->
-  (forall p, M |= [! [idx]p -> [idx][idx]p !]).
-Proof.
-  intros M idx H p.
-
-  (* Step 0: |= X -> ((Y /\ Z) -> (Z /\ X)) -- Tautology *)
-  assert(H0: forall x y z, M |= [! x -> ((y /\ z) -> (z /\ x)) !]) 
-    by (intros x y z w H0;split; destruct H1; trivial).
-
-  (* Step 1: |= [][]X /\ []X -> []([]X /\ X) -- Theorem *)
-  assert(H1: forall x, M |= [! x -> ([idx]([idx]x /\ x) -> ([idx]x /\ x)) !])
-    by (intros x w H1 H2; simpl; split; [apply H2 | assumption]).
-
-  (* Step 2: (|= A -> B) -> (|= []A -> []B) -- Syntatic Property *)
-  assert(H2: forall x y, (M |= [! x -> y !]) -> (M |= [! [idx]x -> [idx]y !]))
-    by (intros x y H2 w H3 w1 H4; apply H2; apply H3; assumption).
-
-  (* Step 3: (|= []X /\ X -> []X) -- Tautology *)
-  assert(H3: forall x, (M |= [! [idx]x /\ x -> [idx]x !]))
-    by (intros ?x ?w H3; apply H3).
-
-  (* Step 4: Prove an instance of Step 0 *)
-  assert(H4: M |= [! p -> (([idx][idx]p /\ [idx]p) -> ([idx]p /\ p)) !])
-    by (apply H0 with (x := [! p !]) (y := [! [idx][idx]p !]) (z := [![idx]p!])); 
-  clear H0.
-
-  (* Step 5: Apply Step 1 on Step 4 *)
-  assert(H5: M |= [! p -> ([idx]([idx]p /\ p) -> ([idx]p /\ p)) !])
-    by (apply H1);
-  clear H1; clear H4.
-
-  (* Step 6: Apply Step 2 on Step 5 *)
-  assert(H6: M |= [! [idx]p -> [idx](([idx]([idx]p /\ p) -> ([idx]p /\ p))) !])
-    by (apply H2; assumption);
-  clear H5.
-
-  (* Step 7: Prove an instance of GL *)
-  assert(H7: M |= [! [idx]([idx]([idx]p /\ p) -> ([idx]p /\ p)) -> [idx]([idx]p /\ p) !])
-    by (apply H with (q := [! [idx]p /\ p !]));
-  clear H.
-
-  (* Step 8: From Step 6 and Step 7, prove |= []p -> []([]p /\ p) 
-  by transitivity of -> *)
-  assert(H8: M |= [! [idx]p -> [idx]([idx]p /\ p) !])
-    by (eapply modal_impl_transitivity; split; [exact H6 | exact H7]);
-  clear H6; clear H7.
-
-  (* Step 9: Prove an instance of Step 3 *)
-  assert(H9: M |= [! [idx]p /\ p -> [idx]p !]) 
-    by (apply H3 with (x := p));
-  clear H3.
-
-  (* Step 10: Apply Step 2 on Step 9 *)
-  assert(H10: M |= [! [idx]([idx]p /\ p) -> [idx][idx]p !])
-    by (auto);
-  clear H2; clear H9.
-
-  (* Step 11: From Step 8 and 10, prove |= []p -> [][]p
-  by transitivity of -> *)
-  assert(H11: M |= [! [idx]p -> [idx][idx]p !])
-    by (eapply modal_impl_transitivity; split; [exact H8 | exact H10]);
-  clear H8; clear H10.
-
-  (* Done. *)
-  assumption.
-Qed.
-
-Theorem axiomGL_implies_noetherian_frame:
-  forall f idx,
-  (forall v p, [f -- v] |= [! [idx]([idx]p -> p) -> [idx]p !]) ->
-  noetherian_frame f idx.
-Proof.
-  intros f idx H.
-  unfold noetherian_frame; split.
-  - apply axiom4_implies_transitive_frame; intros; 
-    apply GL_implies_4; apply H.
-  - generalize dependent H.
-    apply contrapositive.
-    + apply classic.
-    + intros H;
-      unfold conversely_well_founded_frame in H;
-      apply not_all_ex_not in H; destruct H as [S];
-      apply imply_to_and in H; destruct H as [H'' H].
-      assert(H0: forall w, S w -> exists w', ~ (S w' -> ~ R f idx w w')).
-      * intros w2 H3.
-        apply not_ex_all_not with (n:=w2) in H;
-        apply not_and_or in H; destruct H; try contradiction.
-        apply not_all_ex_not in H;
-        destruct H as [w1 H].
-        exists w1; apply H.
-      * destruct H'' as [w H'']; apply not_ex_all_not with (n:=w) in H.
-        apply not_and_or in H; destruct H; try contradiction.
-        apply not_all_ex_not in H;
-        destruct H as [w1 H];
-        apply imply_to_and in H;
-        destruct H as [H''' H]; apply NNPP in H.
-        apply ex_not_not_all;
-        exists (fun _ x => ~ S x);
-        apply ex_not_not_all;
-        exists [! #0 !].
-        intros H1; unfold validate_model in H1; simpl in H1.
-        assert (H2: ~ ([f--(fun _ x => ~ S x)] ' w ||- [! [idx]#0 !])) by
-          (intros H2; apply H2 in H; contradiction);
-        simpl in H2.
-        destruct H1 with (w) (w1); try assumption.
-        intros w2 H3 H4 H5.
-        apply H0 in H5.
-        destruct H5 as [w3 H5].
-        apply imply_to_and in H5.
-        destruct H5 as [H5 H6]; apply NNPP in H6.
-        apply H4 in H6.
+        assumption.
+      + rename x into w4.
         contradiction.
-Qed.
+  Qed.
+
+  Theorem modal_double_neg: 
+    forall M w p, (M ' w ||- [! ~~ p !]) -> (M ' w ||- p).
+  Proof.
+    intros M w p H; simpl in H; apply NNPP; apply H.
+  Qed.
+
+  Theorem modal_contra: 
+    forall M p q,
+    (M |= [! ~ p -> ~ q !]) -> (M |= [! q -> p !]).
+  Proof.
+    intros M p q H w1 H1.
+    unfold validate_model in H; simpl in *.
+    apply modal_double_neg; intros H2.
+    apply H in H2; contradiction.
+  Qed.
+
+  Theorem noetherian_frame_implies_axiomGL:
+    forall f idx,
+    noetherian_frame f idx ->
+    forall v p,
+    [f -- v] |= [! [idx]([idx]p -> p) -> [idx]p !].
+  Proof.
+    intros f idx H v p.
+    apply modal_contra.
+    intros w H1; simpl in w, H1.
+    apply not_all_ex_not in H1; destruct H1 as [w1 H1];
+    apply imply_to_and in H1; destruct H1 as [H1 H2].
+    set (S := fun w1 => R f idx w w1 /\ ([f -- v] ' w1 ||- [! ~ p !])).
+    destruct H as [H H'];
+    destruct H' with S as [w2 [[H3 H4] H5]]; try (exists w1; split; trivial).
+    clear H'; unfold S in H5; clear S.
+    simpl; apply ex_not_not_all.
+    exists w2.
+    intros H6; simpl in H6.
+    apply H6 in H3; try eauto.
+    intros w3 H7.
+    assert (H8: [f-- v] ' w2 ||- [! [idx] p -> p !]) by (intros ?H; apply H6; assumption);
+    assert (H9: [f-- v] ' w2 ||- [! ~ [idx] p !]) by (intros H9; apply H8 in H9; contradiction).
+    simpl in H9; apply not_all_ex_not in H9;
+    destruct H9 as [w4 H9];
+    apply imply_to_and in H9.
+    assert (H10: (R f idx w2 w4 /\ ~([f--v] ' w4 ||- p)) -> (R f idx w2 w4 /\ ([f--v] ' w4 ||- [! ~ p !]))) by (easy);
+    apply H10 in H9; clear H10.
+    assert (H10: R f idx w w4) by (apply H with (w:=w) (w':=w2) (w'':=w4); easy).
+    destruct H9;
+    assert (H11: R f idx w w4 /\ ([f--v] ' w4 ||- [! ~ p !])) by (easy).
+    apply H5 in H11;
+    contradiction.
+  Qed.
+
+  (* Proof adapted from: https://planetmath.org/modallogicgl *)
+  Lemma GL_implies_4:
+    forall M idx,
+    (forall q, M |= [! [idx]([idx]q -> q) -> [idx]q !]) ->
+    (forall p, M |= [! [idx]p -> [idx][idx]p !]).
+  Proof.
+    intros M idx H p.
+
+    (* Step 0: |= X -> ((Y /\ Z) -> (Z /\ X)) -- Tautology *)
+    assert(H0: forall x y z, M |= [! x -> ((y /\ z) -> (z /\ x)) !]) 
+      by (intros x y z w H0;split; destruct H1; trivial).
+
+    (* Step 1: |= [][]X /\ []X -> []([]X /\ X) -- Theorem *)
+    assert(H1: forall x, M |= [! x -> ([idx]([idx]x /\ x) -> ([idx]x /\ x)) !])
+      by (intros x w H1 H2; simpl; split; [apply H2 | assumption]).
+
+    (* Step 2: (|= A -> B) -> (|= []A -> []B) -- Syntatic Property *)
+    assert(H2: forall x y, (M |= [! x -> y !]) -> (M |= [! [idx]x -> [idx]y !]))
+      by (intros x y H2 w H3 w1 H4; apply H2; apply H3; assumption).
+
+    (* Step 3: (|= []X /\ X -> []X) -- Tautology *)
+    assert(H3: forall x, (M |= [! [idx]x /\ x -> [idx]x !]))
+      by (intros ?x ?w H3; apply H3).
+
+    (* Step 4: Prove an instance of Step 0 *)
+    assert(H4: M |= [! p -> (([idx][idx]p /\ [idx]p) -> ([idx]p /\ p)) !])
+      by (apply H0 with (x := [! p !]) (y := [! [idx][idx]p !]) (z := [![idx]p!])); 
+    clear H0.
+
+    (* Step 5: Apply Step 1 on Step 4 *)
+    assert(H5: M |= [! p -> ([idx]([idx]p /\ p) -> ([idx]p /\ p)) !])
+      by (apply H1);
+    clear H1; clear H4.
+
+    (* Step 6: Apply Step 2 on Step 5 *)
+    assert(H6: M |= [! [idx]p -> [idx](([idx]([idx]p /\ p) -> ([idx]p /\ p))) !])
+      by (apply H2; assumption);
+    clear H5.
+
+    (* Step 7: Prove an instance of GL *)
+    assert(H7: M |= [! [idx]([idx]([idx]p /\ p) -> ([idx]p /\ p)) -> [idx]([idx]p /\ p) !])
+      by (apply H with (q := [! [idx]p /\ p !]));
+    clear H.
+
+    (* Step 8: From Step 6 and Step 7, prove |= []p -> []([]p /\ p) 
+    by transitivity of -> *)
+    assert(H8: M |= [! [idx]p -> [idx]([idx]p /\ p) !])
+      by (eapply modal_impl_transitivity; split; [exact H6 | exact H7]);
+    clear H6; clear H7.
+
+    (* Step 9: Prove an instance of Step 3 *)
+    assert(H9: M |= [! [idx]p /\ p -> [idx]p !]) 
+      by (apply H3 with (x := p));
+    clear H3.
+
+    (* Step 10: Apply Step 2 on Step 9 *)
+    assert(H10: M |= [! [idx]([idx]p /\ p) -> [idx][idx]p !])
+      by (auto);
+    clear H2; clear H9.
+
+    (* Step 11: From Step 8 and 10, prove |= []p -> [][]p
+    by transitivity of -> *)
+    assert(H11: M |= [! [idx]p -> [idx][idx]p !])
+      by (eapply modal_impl_transitivity; split; [exact H8 | exact H10]);
+    clear H8; clear H10.
+
+    (* Done. *)
+    assumption.
+  Qed.
+
+  Theorem axiomGL_implies_noetherian_frame:
+    forall f idx,
+    (forall v p, [f -- v] |= [! [idx]([idx]p -> p) -> [idx]p !]) ->
+    noetherian_frame f idx.
+  Proof.
+    intros f idx H.
+    unfold noetherian_frame; split.
+    - apply axiom4_implies_transitive_frame; intros; 
+      apply GL_implies_4; apply H.
+    - generalize dependent H.
+      apply contrapositive.
+      + apply classic.
+      + intros H;
+        unfold conversely_well_founded_frame in H;
+        apply not_all_ex_not in H; destruct H as [S];
+        apply imply_to_and in H; destruct H as [H'' H].
+        assert(H0: forall w, S w -> exists w', ~ (S w' -> ~ R f idx w w')).
+        * intros w2 H3.
+          apply not_ex_all_not with (n:=w2) in H;
+          apply not_and_or in H; destruct H; try contradiction.
+          apply not_all_ex_not in H;
+          destruct H as [w1 H].
+          exists w1; apply H.
+        * destruct H'' as [w H'']; apply not_ex_all_not with (n:=w) in H.
+          apply not_and_or in H; destruct H; try contradiction.
+          apply not_all_ex_not in H;
+          destruct H as [w1 H];
+          apply imply_to_and in H;
+          destruct H as [H''' H]; apply NNPP in H.
+          apply ex_not_not_all;
+          exists (fun _ x => ~ S x);
+          apply ex_not_not_all;
+          exists [! #0 !].
+          intros H1; unfold validate_model in H1; simpl in H1.
+          assert (H2: ~ ([f--(fun _ x => ~ S x)] ' w ||- [! [idx]#0 !])) by
+            (intros H2; apply H2 in H; contradiction);
+          simpl in H2.
+          destruct H1 with (w) (w1); try assumption.
+          intros w2 H3 H4 H5.
+          apply H0 in H5.
+          destruct H5 as [w3 H5].
+          apply imply_to_and in H5.
+          destruct H5 as [H5 H6]; apply NNPP in H6.
+          apply H4 in H6.
+          contradiction.
+  Qed.
+End Validation.
diff --git a/coq/Logical_Equivalence.v b/coq/Logical_Equivalence.v
index 4c18f4b..18ea5eb 100644
--- a/coq/Logical_Equivalence.v
+++ b/coq/Logical_Equivalence.v
@@ -1,107 +1,109 @@
 Require Import Sets Modal_Library Modal_Notations Classical List.
 
-Context `{X: modal_index_set}.
+Section Equivalence.
+  Context `{X: modal_index_set}.
 
-Lemma singleton_formula:
-  forall M p,
-  theory_modal M (Singleton p) -> M |= p.
-Proof.
-  intros.
-  apply H.
-  constructor.
-Qed.
+  Lemma singleton_formula:
+    forall M p,
+    theory_modal M (Singleton p) -> M |= p.
+  Proof.
+    intros.
+    apply H.
+    constructor.
+  Qed.
 
-Theorem implies_to_or_modal:
-  forall φ ψ,
-  [! φ -> ψ !] =|= [! ~φ \/ ψ !].
-Proof.
-  split.
-  - unfold entails_modal, entails, validate_model in *. 
-    intros; simpl in *.
-    apply singleton_formula in H.
-    destruct classic with (M ' w ||- φ); firstorder.
-  - unfold entails_modal, entails in *.
-    intros; simpl in *.
-    apply singleton_formula in H.
-    intro w.
-    specialize (H w).
-    simpl in H.
-    destruct H.
-    + simpl; intros.
-      exfalso; firstorder.
-    + simpl; firstorder.
-Qed.
+  Theorem implies_to_or_modal:
+    forall φ ψ,
+    [! φ -> ψ !] =|= [! ~φ \/ ψ !].
+  Proof.
+    split.
+    - unfold entails_modal, entails, validate_model in *. 
+      intros; simpl in *.
+      apply singleton_formula in H.
+      destruct classic with (M ' w ||- φ); firstorder.
+    - unfold entails_modal, entails in *.
+      intros; simpl in *.
+      apply singleton_formula in H.
+      intro w.
+      specialize (H w).
+      simpl in H.
+      destruct H.
+      + simpl; intros.
+        exfalso; firstorder.
+      + simpl; firstorder.
+  Qed.
 
-Theorem double_neg_modal:
-  forall φ,
-  [! ~~φ !] =|= φ.
-Proof.
-  split.
-  - unfold entails_modal, entails, validate_model; intros.
-    apply singleton_formula in H.
-    specialize (H w); simpl in H.
-    apply NNPP; auto.
-  - unfold entails_modal, entails, validate_model; intros.
-    simpl.
-    apply singleton_formula in H.
-    edestruct classic.
-    + exact H0.
-    + apply NNPP in H0.
-      exfalso; eauto.
-Qed.
+  Theorem double_neg_modal:
+    forall φ,
+    [! ~~φ !] =|= φ.
+  Proof.
+    split.
+    - unfold entails_modal, entails, validate_model; intros.
+      apply singleton_formula in H.
+      specialize (H w); simpl in H.
+      apply NNPP; auto.
+    - unfold entails_modal, entails, validate_model; intros.
+      simpl.
+      apply singleton_formula in H.
+      edestruct classic.
+      + exact H0.
+      + apply NNPP in H0.
+        exfalso; eauto.
+  Qed.
 
-Theorem and_to_implies_modal:
-  forall φ ψ,
-  [! φ /\ ψ !] =|= [! ~(φ -> ~ψ) !].
-Proof.
-  split.
-  - unfold entails_modal, entails, validate_model.
-    simpl in *; intros.
-    unfold validate_model in *.
-    simpl in *.
-    apply singleton_formula in H.
-    unfold not; intros; apply H0.
-    + destruct H with (w:=w); auto.
-    + destruct H with (w:=w); auto.
-  - unfold entails_modal, entails.
-    simpl in *; intros.
-    unfold validate_model in *.
-    intros; simpl in *.
-    apply singleton_formula in H.
-    specialize (H w); simpl in H.
+  Theorem and_to_implies_modal:
+    forall φ ψ,
+    [! φ /\ ψ !] =|= [! ~(φ -> ~ψ) !].
+  Proof.
     split.
-    + edestruct classic.
-      * exact H0.
-      * exfalso.
-        firstorder.
-    + edestruct classic.
-      * exact H0.
-      * firstorder.
-Qed.
+    - unfold entails_modal, entails, validate_model.
+      simpl in *; intros.
+      unfold validate_model in *.
+      simpl in *.
+      apply singleton_formula in H.
+      unfold not; intros; apply H0.
+      + destruct H with (w:=w); auto.
+      + destruct H with (w:=w); auto.
+    - unfold entails_modal, entails.
+      simpl in *; intros.
+      unfold validate_model in *.
+      intros; simpl in *.
+      apply singleton_formula in H.
+      specialize (H w); simpl in H.
+      split.
+      + edestruct classic.
+        * exact H0.
+        * exfalso.
+          firstorder.
+      + edestruct classic.
+        * exact H0.
+        * firstorder.
+  Qed.
 
-Theorem diamond_to_box_modal:
-  forall φ idx,
-  [! <idx>φ !] =|= [! ~[idx]~φ !].
-Proof.
-  split.
-  - unfold entails_modal, entails, validate_model in *.
-    simpl in *; intros.
-    apply singleton_formula in H.
-    specialize (H w); simpl in H.
-    edestruct classic.
-    + exact H0.
-    + firstorder.
-  - intros.
-    unfold entails_modal, entails in *.
-    simpl in *.
-    unfold validate_model in *.
-    simpl in *.
-    unfold not in *.
-    intros.
-    apply singleton_formula in H.
-    specialize (H w); simpl in H.
-    edestruct classic.
-    + exact H0.
-    + exfalso.
-      firstorder.
-Qed.
+  Theorem diamond_to_box_modal:
+    forall φ idx,
+    [! <idx>φ !] =|= [! ~[idx]~φ !].
+  Proof.
+    split.
+    - unfold entails_modal, entails, validate_model in *.
+      simpl in *; intros.
+      apply singleton_formula in H.
+      specialize (H w); simpl in H.
+      edestruct classic.
+      + exact H0.
+      + firstorder.
+    - intros.
+      unfold entails_modal, entails in *.
+      simpl in *.
+      unfold validate_model in *.
+      simpl in *.
+      unfold not in *.
+      intros.
+      apply singleton_formula in H.
+      specialize (H w); simpl in H.
+      edestruct classic.
+      + exact H0.
+      + exfalso.
+        firstorder.
+  Qed.
+End Equivalence.
diff --git a/coq/Makefile b/coq/Makefile
index 11f1e86..07b55a1 100644
--- a/coq/Makefile
+++ b/coq/Makefile
@@ -1,5 +1,5 @@
 ##########################################################################
-##         #   The Coq Proof Assistant / The Coq Development Team       ##
+##         #      The Rocq Prover / The Rocq Development Team           ##
 ##  v      #         Copyright INRIA, CNRS and contributors             ##
 ## <O___,, # (see version control and CREDITS file for authors & dates) ##
 ##   \VV/  ###############################################################
@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.19.0
+## GNUMakefile for Rocq 9.0.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -16,7 +16,7 @@ SELF := $(lastword $(MAKEFILE_LIST))
 PARENT := $(firstword $(MAKEFILE_LIST))
 
 # This file is generated by coq_makefile and contains many variable
-# definitions, like the list of .v files or the path to Coq
+# definitions, like the list of .v files or the path to Rocq
 include Makefile.conf
 
 # Put in place old names
@@ -61,7 +61,7 @@ Makefile.conf: _CoqProject
 # code (be nice to user interfaces).
 
 # Set KEEP_ERROR to have make keep files produced by failing rules.
-# By default, KEEP_ERROR is empty. So for instance if coqc creates a .vo but
+# By default, KEEP_ERROR is empty. So for instance if rocq c creates a .vo but
 # then fails to native compile, the .vo will be deleted.
 # May confuse make so use only for debugging.
 KEEP_ERROR?=
@@ -72,7 +72,7 @@ endif
 # Print shell commands (set to non empty)
 VERBOSE ?=
 
-# Time the Coq process (set to non empty), and how (see default value)
+# Time the Rocq process (set to non empty), and how (see default value)
 TIMED?=
 TIMECMD?=
 # Use command time on linux, gtime on Mac OS
@@ -98,14 +98,15 @@ COQBIN:=$(COQBIN)/
 endif
 
 # Coq binaries
-COQC     ?= "$(COQBIN)coqc"
-COQTOP   ?= "$(COQBIN)coqtop"
-COQCHK   ?= "$(COQBIN)coqchk"
-COQNATIVE ?= "$(COQBIN)coqnative"
-COQDEP   ?= "$(COQBIN)coqdep"
-COQDOC   ?= "$(COQBIN)coqdoc"
-COQPP    ?= "$(COQBIN)coqpp"
-COQMKFILE ?= "$(COQBIN)coq_makefile"
+ROCQ     ?= "$(COQBIN)rocq"
+COQC     ?= "$(COQBIN)rocq" c
+COQTOP   ?= "$(COQBIN)rocq" repl
+COQCHK   ?= "$(COQBIN)rocqchk"
+COQNATIVE ?= "$(COQBIN)rocq" native-precompile
+COQDEP   ?= "$(COQBIN)rocq" dep
+COQDOC   ?= "$(COQBIN)rocq" doc
+COQPP    ?= "$(COQBIN)rocq" pp-mlg
+COQMKFILE ?= "$(COQBIN)rocq" makefile
 OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep"
 
 # Timing scripts
@@ -126,13 +127,13 @@ CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack
 # DESTDIR is prepended to all installation paths
 DESTDIR ?=
 
-# Debug builds, typically -g to OCaml, -debug to Coq.
+# Debug builds, typically -g to OCaml, -debug to Rocq.
 CAMLDEBUG ?=
 COQDEBUG ?=
 
 # Extra packages to be linked in (as in findlib -package)
 CAMLPKGS ?=
-FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS)
+FINDLIBPKGS = -package rocq-runtime.plugins.ltac $(CAMLPKGS)
 
 # Option for making timing files
 TIMING?=
@@ -224,14 +225,12 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
 OPT?=
 
-# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
+# The DYNLIB variable is used by "coqdep -dyndep var" in .v.d
 ifeq '$(OPT)' '-byte'
 USEBYTE:=true
-DYNOBJ:=.cma
 DYNLIB:=.cma
 else
 USEBYTE:=
-DYNOBJ:=.cmxs
 DYNLIB:=.cmxs
 endif
 
@@ -275,10 +274,11 @@ COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS)
 
 COQDOCLIBS?=$(COQLIBS_NOML)
 
-# The version of Coq being run and the version of coq_makefile that
+# The version of Coq being run and the version of rocq makefile that
 # generated this makefile
-COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.19.0
+# NB --print-version is not in the rocq shim
+COQ_VERSION:=$(shell $(ROCQ) c --print-version | cut -d " " -f 1)
+COQMAKEFILE_VERSION:=9.0.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -308,8 +308,8 @@ else
 endif
 
 ifneq (,$(PROFILING))
-  PROFILE_ARG=-profile $<.prof.json
-  PROFILE_ZIP=gzip $<.prof.json
+  PROFILE_ARG=-profile $@.prof.json
+  PROFILE_ZIP=gzip -f $@.prof.json
 else
   PROFILE_ARG=
   PROFILE_ZIP=true
@@ -318,7 +318,7 @@ endif
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
-# Coq project in order to ease the writing of build target and build rules
+# Rocq project in order to ease the writing of build target and build rules
 
 VDFILE := .Makefile.d
 
@@ -397,8 +397,7 @@ FILESTOINSTALL = \
 	$(VOFILES) \
 	$(VFILES) \
 	$(GLOBFILES) \
-	$(NATIVEFILES) \
-	$(CMXSFILES)		# to be removed when we remove legacy loading
+	$(NATIVEFILES)
 FINDLIBFILESTOINSTALL = \
 	$(CMIFILESTOINSTALL)
 ifeq '$(HASNATDYNLINK)' 'true'
@@ -482,8 +481,8 @@ pretty-timed:
 pre-all::
 	@# Extension point
 	$(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
-	  echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
-	  echo "W: while the current Coq version is $(COQ_VERSION)";\
+	  echo "W: This Makefile was generated by Rocq/Coq $(COQMAKEFILE_VERSION)";\
+	  echo "W: while the current Rocq version is $(COQ_VERSION)";\
 	fi
 .PHONY: pre-all
 
@@ -503,37 +502,6 @@ bytefiles: $(CMOFILES) $(CMAFILES)
 optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
 .PHONY: optfiles
 
-# FIXME, see Ralf's bugreport
-# quick is deprecated, now renamed vio
-vio: $(VOFILES:.vo=.vio)
-.PHONY: vio
-quick: vio
-	$(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files")
-.PHONY: quick
-
-vio2vo:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: vio2vo
-
-# quick2vo is undocumented
-quick2vo:
-	$(HIDE)make -j $(J) vio
-	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
-	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
-	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
-	done); \
-	echo "VIO2VO: $$VIOFILES"; \
-	if [ -n "$$VIOFILES" ]; then \
-	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
-	fi
-.PHONY: quick2vo
-
-checkproofs:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: checkproofs
-
 vos: $(VOFILES:%.vo=%.vos)
 .PHONY: vos
 
@@ -541,7 +509,8 @@ vok: $(VOFILES:%.vo=%.vok)
 .PHONY: vok
 
 validate: $(VOFILES)
-	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $(PROFILE_ARG) $^
+	$(HIDE)$(PROFILE_ZIP)
 .PHONY: validate
 
 only: $(TGTS)
@@ -711,9 +680,10 @@ clean::
 	$(HIDE)rm -f $(NATIVEFILES)
 	$(HIDE)find . -name .coq-native -type d -empty -delete
 	$(HIDE)rm -f $(VOFILES)
-	$(HIDE)rm -f $(VOFILES:.vo=.vio)
 	$(HIDE)rm -f $(VOFILES:.vo=.vos)
 	$(HIDE)rm -f $(VOFILES:.vo=.vok)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json.gz)
 	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
 	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
 	$(HIDE)rm -f $(VFILES:.v=.glob)
@@ -817,8 +787,8 @@ define globvorule=
 
 # take care to $$ variables using $< etc
   $(1).vo $(1).glob &: $(1).v | $$(VDFILE)
-	$$(SHOW)COQC $(1).v
-	$$(HIDE)$$(TIMER) $$(COQC) $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v
+	$$(SHOW)ROCQ compile $(1).v
+	$$(HIDE)$$(TIMER) $$(ROCQ) compile $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v
 	$$(HIDE)$$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
 	$$(SHOW)COQNATIVE $(1).vo
@@ -829,8 +799,8 @@ endef
 else
 
 $(VOFILES): %.vo: %.v | $(VDFILE)
-	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(SHOW)ROCQ compile $<
+	$(HIDE)$(TIMER) $(ROCQ) compile $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $<
 	$(HIDE)$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
@@ -839,24 +809,20 @@ endif
 
 # this is broken :( todo fix if we ever find a solution that doesn't need grouped targets
 $(GLOBFILES): %.glob: %.v
-	$(SHOW)'COQC $< (for .glob)'
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+	$(SHOW)'ROCQ compile $< (for .glob)'
+	$(HIDE)$(TIMER) $(ROCQ) compile $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 endif
 
 $(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile))))
 
-$(VFILES:.v=.vio): %.vio: %.v
-	$(SHOW)COQC -vio $<
-	$(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
 $(VFILES:.v=.vos): %.vos: %.v
-	$(SHOW)COQC -vos $<
-	$(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+	$(SHOW)ROCQ compile -vos $<
+	$(HIDE)$(TIMER) $(ROCQ) compile -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 $(VFILES:.v=.vok): %.vok: %.v
-	$(SHOW)COQC -vok $<
-	$(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+	$(SHOW)ROCQ compile -vok $<
+	$(HIDE)$(TIMER) $(ROCQ) compile -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
 	$(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing
@@ -864,7 +830,7 @@ $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-tim
 
 $(BEAUTYFILES): %.v.beautified: %.v
 	$(SHOW)'BEAUTIFY $<'
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
+	$(HIDE)$(TIMER) $(ROCQ) compile $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
 
 $(TEXFILES): %.tex: %.v
 	$(SHOW)'COQDOC -latex $<'
@@ -925,8 +891,8 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
 VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
 
 $(VDFILE): _CoqProject $(VFILES)
-	$(SHOW)'COQDEP VFILES'
-	$(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+	$(SHOW)'ROCQ DEP VFILES'
+	$(HIDE)$(TIMER) $(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
 
 # Misc ########################################################################
 

From 3a2f09e2989133c940963ea4e4caf7d7fc7b566d Mon Sep 17 00:00:00 2001
From: Elian Babireski <elian.babireski@gmail.com>
Date: Tue, 15 Apr 2025 15:36:53 -0300
Subject: [PATCH 2/2] Change gamma lookalike for true gamma

---
 coq/Deductive_System.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/coq/Deductive_System.v b/coq/Deductive_System.v
index f6587f8..a4882b0 100644
--- a/coq/Deductive_System.v
+++ b/coq/Deductive_System.v
@@ -30,14 +30,14 @@ Inductive axiom: Set :=
 Definition instantiate (a: axiom): formula :=
   match a with
   | ax1      φ ψ   => [! φ -> (ψ -> φ) !]
-  | ax2      φ ψ Ɣ => [! (φ -> (ψ -> Ɣ)) -> ((φ -> ψ) -> (φ -> Ɣ)) !]
+  | ax2      φ ψ γ => [! (φ -> (ψ -> γ)) -> ((φ -> ψ) -> (φ -> γ)) !]
   | ax3      φ ψ   => [! (~ψ -> ~φ) -> (φ -> ψ) !]
   | ax4      φ ψ   => [! φ -> (ψ -> (φ /\ ψ)) !]
   | ax5      φ ψ   => [! (φ /\ ψ) -> φ !]
   | ax6      φ ψ   => [! (φ /\ ψ) -> ψ !]
   | ax7      φ ψ   => [! φ -> (φ \/ ψ) !]
   | ax8      φ ψ   => [! ψ -> (φ \/ ψ) !]
-  | ax9      φ ψ Ɣ => [! (φ -> Ɣ) -> ((ψ -> Ɣ) -> ((φ \/ ψ) -> Ɣ)) !]
+  | ax9      φ ψ γ => [! (φ -> γ) -> ((ψ -> γ) -> ((φ \/ ψ) -> γ)) !]
   | ax10     φ     => [! ~~φ -> φ !]
   | axK    i φ ψ   => [! [i](φ -> ψ) -> ([i]φ -> [i]ψ) !]
   | axDual i φ     => [! <i>φ <-> ~[i]~φ !]