theorem
proved
exactPathClass_zero_subsingleton_or_the_precise_finite_head_fact
show as:
exactPathClass_zero_subsingleton_or_the_precise_finite_head_fact