induction F
F : Formula
σ : Instantiation
τ τ' : MetaInstantiation
h1 : F.metaVarSet = ∅
⊢ sub σ τ F = sub σ τ' F
case meta_var_
σ : Instantiation
τ τ' : MetaInstantiation
a✝ : MetaVarName
h1 : (meta_var_ a✝).metaVarSet = ∅
⊢ sub σ τ (meta_var_ a✝) = sub σ τ' (meta_var_ a✝)

case pred_
σ : Instantiation
τ τ' : MetaInstantiation
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_ a✝¹ a✝).metaVarSet = ∅
⊢ sub σ τ (pred_ a✝¹ a✝) = sub σ τ' (pred_ a✝¹ a✝)

case eq_
σ : Instantiation
τ τ' : MetaInstantiation
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).metaVarSet = ∅
⊢ sub σ τ (eq_ a✝¹ a✝) = sub σ τ' (eq_ a✝¹ a✝)

case true_
σ : Instantiation
τ τ' : MetaInstantiation
h1 : true_.metaVarSet = ∅
⊢ sub σ τ true_ = sub σ τ' true_

case not_
σ : Instantiation
τ τ' : MetaInstantiation
a✝ : Formula
a_ih✝ : a✝.metaVarSet = ∅ → sub σ τ a✝ = sub σ τ' a✝
h1 : a✝.not_.metaVarSet = ∅
⊢ sub σ τ a✝.not_ = sub σ τ' a✝.not_

case imp_
σ : Instantiation
τ τ' : MetaInstantiation
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.metaVarSet = ∅ → sub σ τ a✝¹ = sub σ τ' a✝¹
a_ih✝ : a✝.metaVarSet = ∅ → sub σ τ a✝ = sub σ τ' a✝
h1 : (a✝¹.imp_ a✝).metaVarSet = ∅
⊢ sub σ τ (a✝¹.imp_ a✝) = sub σ τ' (a✝¹.imp_ a✝)

case forall_
σ : Instantiation
τ τ' : MetaInstantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.metaVarSet = ∅ → sub σ τ a✝ = sub σ τ' a✝
h1 : (forall_ a✝¹ a✝).metaVarSet = ∅
⊢ sub σ τ (forall_ a✝¹ a✝) = sub σ τ' (forall_ a✝¹ a✝)

case def_
σ : Instantiation
τ τ' : MetaInstantiation
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).metaVarSet = ∅
⊢ sub σ τ (def_ a✝¹ a✝) = sub σ τ' (def_ a✝¹ a✝)