Theorem: FOL.NV.Holds_iff_alphaEqv_Holds (FOL/NV/Alpha.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F F' : Formula
h1 : AlphaEqv F F'
⊢ Holds D I V E F ↔ Holds D I V E F'
Tactic:
induction h1 generalizing V
State after:
case rename_forall_
D : Type
I : Interpretation D
E : Env
F F' phi✝ : Formula
x✝ y✝ : VarName
a✝¹ : ¬isFreeIn y✝ phi✝
a✝ : ¬isBoundIn y✝ phi✝
V : VarAssignment D
⊢ Holds D I V E (forall_ x✝ phi✝) ↔ Holds D I V E (forall_ y✝ (Sub.Var.One.Rec.fastReplaceFree x✝ y✝ phi✝))

case rename_exists_
D : Type
I : Interpretation D
E : Env
F F' phi✝ : Formula
x✝ y✝ : VarName
a✝¹ : ¬isFreeIn y✝ phi✝
a✝ : ¬isBoundIn y✝ phi✝
V : VarAssignment D
⊢ Holds D I V E (exists_ x✝ phi✝) ↔ Holds D I V E (exists_ y✝ (Sub.Var.One.Rec.fastReplaceFree x✝ y✝ phi✝))

case compat_not_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ : Formula
a✝ : AlphaEqv phi✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I V E phi✝.not_ ↔ Holds D I V E phi'✝.not_

case compat_imp_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv psi✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I V E (phi✝.imp_ psi✝) ↔ Holds D I V E (phi'✝.imp_ psi'✝)

case compat_and_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv psi✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I V E (phi✝.and_ psi✝) ↔ Holds D I V E (phi'✝.and_ psi'✝)

case compat_or_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv psi✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I V E (phi✝.or_ psi✝) ↔ Holds D I V E (phi'✝.or_ psi'✝)

case compat_iff_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv psi✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I V E (phi✝.iff_ psi✝) ↔ Holds D I V E (phi'✝.iff_ psi'✝)

case compat_forall_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ : Formula
x✝ : VarName
a✝ : AlphaEqv phi✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I V E (forall_ x✝ phi✝) ↔ Holds D I V E (forall_ x✝ phi'✝)

case compat_exists_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ : Formula
x✝ : VarName
a✝ : AlphaEqv phi✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I V E (exists_ x✝ phi✝) ↔ Holds D I V E (exists_ x✝ phi'✝)

case refl_
D : Type
I : Interpretation D
E : Env
F F' phi✝ : Formula
V : VarAssignment D
⊢ Holds D I V E phi✝ ↔ Holds D I V E phi✝

case symm_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ : Formula
a✝ : AlphaEqv phi✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I V E phi'✝ ↔ Holds D I V E phi✝

case trans_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ phi''✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv phi'✝ phi''✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi'✝ ↔ Holds D I V E phi''✝
V : VarAssignment D
⊢ Holds D I V E phi✝ ↔ Holds D I V E phi''✝

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_y (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi))
Tactic:
case rename_forall_ h1_phi h1_x h1_y h1_1 h1_2 | rename_exists_ h1_phi h1_x h1_y h1_1 h1_2 =>
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  exact replace_empty_Holds D I V E h1_x h1_y h1_phi d h1_1 h1_2
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
Tactic:
case compat_not_ h1_phi h1_phi' _ h1_ih =>
  simp only [Holds]
  congr! 1
  exact h1_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_psi)
Tactic:
case compat_forall_ h1_phi h1_psi h1_x _ h1_ih | compat_exists_ h1_phi h1_psi h1_x _ h1_ih =>
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  exact h1_ih (Function.updateITE V h1_x d)
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1 : Formula
V : VarAssignment D
⊢ Holds D I V E h1 ↔ Holds D I V E h1
Tactic:
case refl_ h1 =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi' ↔ Holds D I V E h1_phi
Tactic:
case symm_ h1_phi h1_phi' _ h1_ih =>
  symm
  exact h1_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_y (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_y a) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)

State before:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_y a) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)

State before:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi ↔
    Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
exact replace_empty_Holds D I V E h1_x h1_y h1_phi d h1_1 h1_2
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ (∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_y a) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∃ d, Holds D I (Function.updateITE V h1_y d) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi : Formula
h1_x h1_y : VarName
h1_1 : ¬isFreeIn h1_y h1_phi
h1_2 : ¬isBoundIn h1_y h1_phi
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V h1_x a) E h1_phi ↔
      Holds D I (Function.updateITE V h1_y a) E (Sub.Var.One.Rec.fastReplaceFree h1_x h1_y h1_phi)

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I V E h1_phi ↔ ¬Holds D I V E h1_phi'

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I V E h1_phi ↔ ¬Holds D I V E h1_phi'
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
exact h1_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E (h1_phi.iff_ h1_psi) ↔ Holds D I V E (h1_phi'.iff_ h1_psi')
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ (Holds D I V E h1_phi ↔ Holds D I V E h1_psi) ↔ (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi')

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ (Holds D I V E h1_phi ↔ Holds D I V E h1_psi) ↔ (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi')
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E h1_psi ↔ Holds D I V E h1_psi'

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
exact h1_ih_1 V
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
Tactic:
exact h1_ih_2 V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_psi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔ ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_psi

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔ ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_psi
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi

State before:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) E h1_psi

State before:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) E h1_psi
Tactic:
exact h1_ih (Function.updateITE V h1_x d)
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_psi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔ ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_psi
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi

State before:
D : Type
I : Interpretation D
E : Env
F F' h1 : Formula
V : VarAssignment D
⊢ Holds D I V E h1 ↔ Holds D I V E h1
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi' ↔ Holds D I V E h1_phi
Tactic:
symm
State after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
exact h1_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi''
Tactic:
trans Holds D I V E h1_phi'
State after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'

D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
exact h1_ih_1 V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
Tactic:
exact h1_ih_2 V
State after:
no goals