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

State before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admits t v (replaceFree v t F)
Tactic:
simp only [replaceFree]
State after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admits t v (replaceFreeAux v t ∅ F)

State before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admits t v (replaceFreeAux v t ∅ F)
Tactic:
simp only [admits]
State after:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admitsAux t v ∅ (replaceFreeAux v t ∅ F)

State before:
F : Formula
v t : VarName
h1 : ¬occursIn t F
⊢ admitsAux t v ∅ (replaceFreeAux v t ∅ F)
Tactic:
exact replaceFreeAux_admitsAux F v t ∅ h1
State after:
no goals