proposition: Lemma precompose_pconst {A B C : pType} (f : B ->* C) : f o* @pconst A B ==* pconst.
proof: Proof. srapply Build_pHomotopy. 1: intro; apply point_eq. exact (concat_p1 _ @ concat_1p _)^. Defined.
imports: Basics Types Pointed.Core