split
case add
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
⊢ (match typecheck l, typecheck r with
      | Maybe.found Ty.nat lth, Maybe.found Ty.nat rth => Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat)
      | x, x_1 => Maybe.unknown) =
      Maybe.unknown →
    ∀ (t : Ty), ¬HasType (add l r) t
case add.h_1
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝¹ : {{t|HasType l t}}
x✝ : {{t|HasType r t}}
lth✝ : HasType l Ty.nat
rth✝ : HasType r Ty.nat
heq✝¹ : typecheck l = Maybe.found Ty.nat lth✝
heq✝ : typecheck r = Maybe.found Ty.nat rth✝
⊢ Maybe.found Ty.nat (_ : HasType (add l r) Ty.nat) = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t

case add.h_2
l r : Exp
lih : typecheck l = Maybe.unknown → ∀ (t : Ty), ¬HasType l t
rih : typecheck r = Maybe.unknown → ∀ (t : Ty), ¬HasType r t
x✝² : {{t|HasType l t}}
x✝¹ : {{t|HasType r t}}
x✝ :
  ∀ (lth : HasType l Ty.nat) (rth : HasType r Ty.nat),
    typecheck l = Maybe.found Ty.nat lth → typecheck r = Maybe.found Ty.nat rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (add l r) t