exact h1
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
no goals