`{O : ReflectiveSubuniverse} {X Y : pType} `{In O Y} (f : X ->* Y) : pO_rec f o* pto O X ==* f. Proof. srapply Build_pHomotopy. 1: nrapply O_rec_beta. cbn. apply moveL_pV. exact (concat_1p _)^. Defined.
Require Import Basics Types ReflectiveSubuniverse Pointed.Core.