case and.h_1 _ _ htl htr rl rr =>
  intros
  contradiction
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}}
htl : HasType l Ty.bool
htr : HasType r Ty.bool
rl : typecheck l = Maybe.found Ty.bool htl
rr : typecheck r = Maybe.found Ty.bool htr
⊢ Maybe.found Ty.bool (_ : HasType (and l r) Ty.bool) = Maybe.unknown → ∀ (t : Ty), ¬HasType (and l r) t
no goals