induction F generalizing V
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ E
h2 : IsMetaVarOrAllDefInEnv E F
h3 : E'.Nodup
⊢ Holds D I V M E' F ↔ Holds D I V M E F
case meta_var_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝ : MetaVarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (meta_var_ a✝)
⊢ Holds D I V M E' (meta_var_ a✝) ↔ Holds D I V M E (meta_var_ a✝)

case pred_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ : PredName
a✝ : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)
⊢ Holds D I V M E' (pred_ a✝¹ a✝) ↔ Holds D I V M E (pred_ a✝¹ a✝)

case eq_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ a✝ : VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)
⊢ Holds D I V M E' (eq_ a✝¹ a✝) ↔ Holds D I V M E (eq_ a✝¹ a✝)

case true_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I V M E' true_ ↔ Holds D I V M E true_

case not_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝ : Formula
a_ih✝ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝ → (Holds D I V M E' a✝ ↔ Holds D I V M E a✝)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E a✝.not_
⊢ Holds D I V M E' a✝.not_ ↔ Holds D I V M E a✝.not_

case imp_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝¹ → (Holds D I V M E' a✝¹ ↔ Holds D I V M E a✝¹)
a_ih✝ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝ → (Holds D I V M E' a✝ ↔ Holds D I V M E a✝)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)
⊢ Holds D I V M E' (a✝¹.imp_ a✝) ↔ Holds D I V M E (a✝¹.imp_ a✝)

case forall_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝ → (Holds D I V M E' a✝ ↔ Holds D I V M E a✝)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)
⊢ Holds D I V M E' (forall_ a✝¹ a✝) ↔ Holds D I V M E (forall_ a✝¹ a✝)

case def_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ : DefName
a✝ : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)
⊢ Holds D I V M E' (def_ a✝¹ a✝) ↔ Holds D I V M E (def_ a✝¹ a✝)