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
v : VarName
a1 : 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
Tactic:
apply Function.updateListITE_mem_eq_len
Proof state after:
case s2.h1
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 : VarName
a1 : v ∈ E_hd.args
⊢ v ∈ E_hd.args

case s2.h2
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 : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = (List.map (V ∘ ↑σ) xs).length

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