case true_ =>
  simp only [Holds]
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_
no goals