Require Import GQM.Base.
Require Import GQM.GQM.
Require Import GQM.GQMDeduction.
Require Import GQM.GQMClassical.

Lemma lemma_5_2 : forall A, (|-- [A]A <<->> [A](A.[change_top (Var 0)])).
Proof.
  (* trivial, but need functional extensionality*)
Abort.

Lemma lemma_A_1 : forall A B, |-- A ->> B -> |-- [A](A.[ren(+1)]) ->> [A](B.[ren(+1)]).
  move => A B HA.
  have HB := (gqm_Anec _ HA).
  eauto with GQMDB.
Qed.