intro h t ht
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}}
hnp :
  ∀ (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
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}}
hnp :
  ∀ (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
h : Maybe.unknown = Maybe.unknown
t : Ty
ht : HasType (and l r) t
⊢ False