induction F
E : Env
σ : Instantiation
τ : MetaInstantiation
F : Formula
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ F)
⊢ IsMetaVarOrAllDefInEnv E F
case meta_var_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ a✝))
⊢ IsMetaVarOrAllDefInEnv E (meta_var_ a✝)

case pred_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : PredName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ a✝¹ a✝))
⊢ IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)

case eq_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ a✝¹ a✝))
⊢ IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)

case true_
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ true_)
⊢ IsMetaVarOrAllDefInEnv E true_

case not_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : Formula
a_ih✝ : IsMetaVarOrAllDefInEnv E (sub σ τ a✝) → IsMetaVarOrAllDefInEnv E a✝
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ a✝.not_)
⊢ IsMetaVarOrAllDefInEnv E a✝.not_

case imp_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : Formula
a_ih✝¹ : IsMetaVarOrAllDefInEnv E (sub σ τ a✝¹) → IsMetaVarOrAllDefInEnv E a✝¹
a_ih✝ : IsMetaVarOrAllDefInEnv E (sub σ τ a✝) → IsMetaVarOrAllDefInEnv E a✝
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (a✝¹.imp_ a✝))
⊢ IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)

case forall_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ : IsMetaVarOrAllDefInEnv E (sub σ τ a✝) → IsMetaVarOrAllDefInEnv E a✝
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ a✝¹ a✝))
⊢ IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)

case def_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝¹ : DefName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (def_ a✝¹ a✝))
⊢ IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)