induction F
E : Env
σ : Instantiation
τ : MetaInstantiation
F : Formula
h1 : IsMetaVarOrAllDefInEnv E F
h2 : ∀ X ∈ F.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ F)
case meta_var_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ a✝)
h2 : ∀ X ∈ (meta_var_ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ a✝))

case pred_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : PredName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)
h2 : ∀ X ∈ (pred_ a✝¹ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ a✝¹ a✝))

case eq_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)
h2 : ∀ X ∈ (eq_ a✝¹ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ a✝¹ a✝))

case true_
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ true_)

case not_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : Formula
a_ih✝ :
  IsMetaVarOrAllDefInEnv E a✝ →
    (∀ X ∈ a✝.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ a✝)
h1 : IsMetaVarOrAllDefInEnv E a✝.not_
h2 : ∀ X ∈ a✝.not_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ a✝.not_)

case imp_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : Formula
a_ih✝¹ :
  IsMetaVarOrAllDefInEnv E a✝¹ →
    (∀ X ∈ a✝¹.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ a✝¹)
a_ih✝ :
  IsMetaVarOrAllDefInEnv E a✝ →
    (∀ X ∈ a✝.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ a✝)
h1 : IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)
h2 : ∀ X ∈ (a✝¹.imp_ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (a✝¹.imp_ a✝))

case forall_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  IsMetaVarOrAllDefInEnv E a✝ →
    (∀ X ∈ a✝.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ a✝)
h1 : IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)
h2 : ∀ X ∈ (forall_ a✝¹ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ a✝¹ a✝))

case def_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : DefName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)
h2 : ∀ X ∈ (def_ a✝¹ a✝).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ a✝¹ a✝))