(Q : Type) (scct' : forall a (x : C a), Q) (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y)) (b:B) (y: C (f b)) : ap (sWtil_rec Q scct' sppt') (sppt b y) = sppt' b y. Proof. unfold sWtil_rec, sppt. refine (@ap_sig_rec_path_sigma W' P Q _ _ (cglue b) _ _ _ _ @ _); simpl. rewrite (@Coeq_ind_beta_cglue B A f g). rewrite (ap10_dpath_arrow P (fun _ => Q) (cglue b) _ _ _ y). repeat rewrite concat_p_pp. rewrite ap_V, concat_pV_p, concat_pV_p, concat_pV_p, concat_Vp. by apply concat_1p. Qed.
Require Import HoTT.Basics. Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe. Require Import HoTT.Colimits.Coeq.