Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
F : Formula
h1 : IsMetaVarOrAllDefInEnv E F
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E F ↔ Holds D I V M E (sub σ τ F)
Tactic:
induction F generalizing V
Proof state after:
case meta_var_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝ : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ a✝) ↔
    Holds D I V M E (sub σ τ (meta_var_ a✝))

case pred_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ : PredName
a✝ : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ a✝¹ a✝) ↔
    Holds D I V M E (sub σ τ (pred_ a✝¹ a✝))

case eq_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ a✝ : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ a✝¹ a✝) ↔
    Holds D I V M E (sub σ τ (eq_ a✝¹ a✝))

case true_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E (sub σ τ true_)

case not_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝ : Formula
a_ih✝ :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E a✝ →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝ ↔ Holds D I V M E (sub σ τ a✝))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E a✝.not_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝.not_ ↔ Holds D I V M E (sub σ τ a✝.not_)

case imp_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E a✝¹ →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝¹ ↔ Holds D I V M E (sub σ τ a✝¹))
a_ih✝ :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E a✝ →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝ ↔ Holds D I V M E (sub σ τ a✝))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (a✝¹.imp_ a✝) ↔
    Holds D I V M E (sub σ τ (a✝¹.imp_ a✝))

case forall_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E a✝ →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝ ↔ Holds D I V M E (sub σ τ a✝))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ a✝¹ a✝) ↔
    Holds D I V M E (sub σ τ (forall_ a✝¹ a✝))

case def_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ : DefName
a✝ : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (def_ a✝¹ a✝) ↔
    Holds D I V M E (sub σ τ (def_ a✝¹ a✝))