proposition: Lemma wedge_up X Y Z (f g : X \/ Y $-> Z) : f $o wedge_inl $== g $o wedge_inl -> f $o wedge_inr $== g $o wedge_inr -> f $== g.
proof: Proof. intros p q. snrapply Build_pHomotopy. - snrapply (Pushout_ind _ p q). intros []. simpl. refine (transport_paths_FlFr _ _ @ _). refine (concat_pp_p _ _ _ @ _). apply moveR_Vp. refine (whiskerR (dpoint_eq p) _ @ _). refine (_ @ whiskerL _ (dpoint_eq q)^). clear p q. simpl. apply moveL_Mp. rewrite ? ap_V. rewrite ? inv_pp. hott_simpl. - simpl; pelim p q. hott_simpl. Defined.
imports: Basics Types Pointed.Core Pointed.pSusp Colimits.Pushout WildCat Homotopy.Suspension