case unit
a b✝ c d : Prop
b : PUnit
⊢ unit = b
a✝ b✝ c d : Prop
a b : PUnit
⊢ a = b
cases a
case unit.unit
a b c d : Prop
⊢ unit = unit
case unit
a b✝ c d : Prop
b : PUnit
⊢ unit = b
cases b
no goals
case unit.unit
a b c d : Prop
⊢ unit = unit
exact rfl