case true_ =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ true_)
no goals