have baldie := add_one_hair_still_bald ih
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
⊢ head✝ :: h = ∅
case cons
person : Person
head✝ : Strand
h : List Strand
ih : h = ∅
baldie : Bald (add_one_hair { hair := h })
⊢ head✝ :: h = ∅