theorem typing_unique (t : Trm) : t.lc → ∀ (Γ : context) (T1 T2 : Typ), typing Γ t T1 → typing Γ t T2 → T1 = T2

theorem typing_decidable (t : Trm) (Γ : context) : t.lc → valid_ctx Γ → (∃ (T : Typ), typing Γ t T) ∨ ¬∃ (T : Typ), typing Γ t T

theorem typechecking_decidable (t : Trm) (T : Typ) (Γ : context) : t.lc → valid_ctx Γ → typing Γ t T ∨ ¬typing Γ t T