Skip to content
Snippets Groups Projects
Normal view Permalink
Section5.v 417 B
Newer Older
  • Learn to ignore specific revisions
    • Mackie Loeffel's avatar
    started section 5
    Mackie Loeffel committed
    1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 
    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.