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

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

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

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

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

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

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

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