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

State before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmits t v (fastReplaceFree v t F)
Tactic:
simp only [fastAdmits]
State after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmitsAux t v ∅ (fastReplaceFree v t F)

State before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ fastAdmitsAux t v ∅ (fastReplaceFree v t F)
Tactic:
apply fastReplaceFree_aux_fastAdmitsAux F v t ∅ h1
State after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ v ∉ ∅

State before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ v ∉ ∅
Tactic:
simp
State after:
no goals