Supporting results for pointwise provable equality.

theorem PointwiseComposition.Empty.eq_elim {α : Sort u} (f : Empty → α) : f = Empty.elim