{ exact hab }
case h₁
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = ?b

case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ ?b = c

case b
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ α
case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c