cases typecheck e with
| found t2 ht2 =>
  intros
  have h : t = t2 := HasType_det ht1 ht2
  simp [h]
| unknown =>
  intros
  contradiction
e : Exp
t : Ty
h ht1 : HasType e t
⊢ typecheck e ≠ Maybe.unknown → typecheck e = Maybe.found t h
no goals