Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem (FOL/NV/Sub/Pred/All/Rec/Option/Fresh/Sub.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ Holds D (I' D I V E τ) V E F ↔ Holds D I V E (sub c τ F)
Tactic:
apply substitution_theorem_aux
State after:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ (x : VarName), isFreeIn x F → V x = V (id x)

case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ x ∈ F.predVarSet.biUnion (predVarFreeVarSet τ), V x = V x

State before:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ (x : VarName), isFreeIn x F → V x = V (id x)
Tactic:
simp
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ x ∈ F.predVarSet.biUnion (predVarFreeVarSet τ), V x = V x
Tactic:
simp
State after:
no goals