split
case and
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.bool lth, Maybe.found Ty.bool rth => Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool)
      | x, x_1 => Maybe.unknown) =
      Maybe.unknown →
    ∀ (t : Ty), ¬HasType (and l r) t
case and.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.bool
rth✝ : HasType r Ty.bool
heq✝¹ : typecheck l = Maybe.found Ty.bool lth✝
heq✝ : typecheck r = Maybe.found Ty.bool rth✝
⊢ Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t

case and.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.bool) (rth : HasType r Ty.bool),
    typecheck l = Maybe.found Ty.bool lth → typecheck r = Maybe.found Ty.bool rth → False
⊢ Maybe.unknown = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t