Theorem: Cpdt.Chapter5.HasType_det (Cpdt/Chapter5/Typechecker.lean)

State before:
e : Exp
t1 t2 : Ty
⊢ HasType e t1 → HasType e t2 → t1 = t2
Tactic:
intro h1 h2
State after:
e : Exp
t1 t2 : Ty
h1 : HasType e t1
h2 : HasType e t2
⊢ t1 = t2

State before:
e : Exp
t1 t2 : Ty
h1 : HasType e t1
h2 : HasType e t2
⊢ t1 = t2
Tactic:
cases h1 <;> cases h2 <;> rfl
State after:
no goals