intros
case unknown
e : Exp
t : Ty
h ht1 : HasType e t
⊢ Maybe.unknown ≠ Maybe.unknown → Maybe.unknown = Maybe.found t h
case unknown
e : Exp
t : Ty
h ht1 : HasType e t
a✝ : Maybe.unknown ≠ Maybe.unknown
⊢ Maybe.unknown = Maybe.found t h