Γ ⊢ p = { t₀ : *, t₁ : *, ... tₙ : * }
Γ ⊢ c = { ... }
T ∉ dom(Γ)
───────────────────────────────────────────
Γ, T ⊢ [variant T p f] : *₀ → *₁ → ... → *ₙ

TypeDeclareVariant