induction F
F : Formula
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ F) = sub (σ.comp σ') meta_var_ F
case meta_var_
σ σ' : Instantiation
a✝ : MetaVarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (meta_var_ a✝)) = sub (σ.comp σ') meta_var_ (meta_var_ a✝)

case pred_
σ σ' : Instantiation
a✝¹ : PredName
a✝ : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (pred_ a✝¹ a✝)) = sub (σ.comp σ') meta_var_ (pred_ a✝¹ a✝)

case eq_
σ σ' : Instantiation
a✝¹ a✝ : VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (eq_ a✝¹ a✝)) = sub (σ.comp σ') meta_var_ (eq_ a✝¹ a✝)

case true_
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ true_) = sub (σ.comp σ') meta_var_ true_

case not_
σ σ' : Instantiation
a✝ : Formula
a_ih✝ : sub σ meta_var_ (sub σ' meta_var_ a✝) = sub (σ.comp σ') meta_var_ a✝
⊢ sub σ meta_var_ (sub σ' meta_var_ a✝.not_) = sub (σ.comp σ') meta_var_ a✝.not_

case imp_
σ σ' : Instantiation
a✝¹ a✝ : Formula
a_ih✝¹ : sub σ meta_var_ (sub σ' meta_var_ a✝¹) = sub (σ.comp σ') meta_var_ a✝¹
a_ih✝ : sub σ meta_var_ (sub σ' meta_var_ a✝) = sub (σ.comp σ') meta_var_ a✝
⊢ sub σ meta_var_ (sub σ' meta_var_ (a✝¹.imp_ a✝)) = sub (σ.comp σ') meta_var_ (a✝¹.imp_ a✝)

case forall_
σ σ' : Instantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ : sub σ meta_var_ (sub σ' meta_var_ a✝) = sub (σ.comp σ') meta_var_ a✝
⊢ sub σ meta_var_ (sub σ' meta_var_ (forall_ a✝¹ a✝)) = sub (σ.comp σ') meta_var_ (forall_ a✝¹ a✝)

case def_
σ σ' : Instantiation
a✝¹ : DefName
a✝ : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (def_ a✝¹ a✝)) = sub (σ.comp σ') meta_var_ (def_ a✝¹ a✝)