simp only
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
h2 : ∀ X_1 ∈ (pred_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ True
no goals