have still_bald := add_one_hair_still_bald bald
baldie : Person := { hair := [] }
bald : Bald baldie
⊢ False
baldie : Person := { hair := [] }
bald : Bald baldie
still_bald : Bald (add_one_hair baldie)
⊢ False