Theorem: MM0.holds_sub
Proof state before:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
apply holds_coincide_var D I (Function.updateListITE (V ∘ σ.val) E_hd.args (List.map (V ∘ σ.val) xs)) (Function.updateListITE V E_hd.args (List.map (V ∘ σ.val) xs)) M E_tl E_hd.F E_hd.args E_hd.nf
Proof state after:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ ∀ v ∈ E_hd.args,
    Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs) v =
      Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs) v

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F