Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem (FOL/NV/Sub/Var/One/Rec/Admits.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmits v t F
⊢ Holds D I (Function.updateITE V v (V t)) E F ↔ Holds D I V E (fastReplaceFree v t F)
Tactic:
simp only [fastAdmits] at h1
State after:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmitsAux v t ∅ F
⊢ Holds D I (Function.updateITE V v (V t)) E F ↔ Holds D I V E (fastReplaceFree v t F)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmitsAux v t ∅ F
⊢ Holds D I (Function.updateITE V v (V t)) E F ↔ Holds D I V E (fastReplaceFree v t F)
Tactic:
apply substitution_theorem_aux D I V V E v t ∅ F h1
State after:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmitsAux v t ∅ F
⊢ ∀ v ∉ ∅, V v = V v

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
v t : VarName
F : Formula
h1 : fastAdmitsAux v t ∅ F
⊢ ∀ v ∉ ∅, V v = V v
Tactic:
simp
State after:
no goals