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

TypeDeclareRecord