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