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

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let zs := (τ X ds.length).1;
          let H := (τ X ds.length).2;
          if ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ X ds }
      V E F ↔
    Holds D I V E (replace τ F)
Tactic:
apply substitution_theorem_aux D I V V E τ ∅ F
State after:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ admitsAux τ ∅ F

case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ ∀ x ∉ ∅, V x = V x

State before:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ admitsAux τ ∅ F
Tactic:
simp only [admits] at h1
State after:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admitsAux τ ∅ F
⊢ admitsAux τ ∅ F

State before:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admitsAux τ ∅ F
⊢ admitsAux τ ∅ F
Tactic:
exact h1
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ ∀ x ∉ ∅, V x = V x
Tactic:
intro X _
State after:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
X : VarName
a✝ : X ∉ ∅
⊢ V X = V X

State before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
X : VarName
a✝ : X ∉ ∅
⊢ V X = V X
Tactic:
rfl
State after:
no goals