rw [Bald, add_one_hair] at still_bald
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : Bald (add_one_hair baldie)
⊢ False
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : { hair := Strand.strand :: baldie.hair }.hair = ∅
⊢ False