{A B f g C} {D : forall b, C (f b) <~> C (g b)} (Q : Type) (cct' : forall a (x : C a), Q) (ppt' : forall (b:B) (y : C (f b)), cct' (f b) y = cct' (g b) (D b y)) (b:B) (y: C (f b)) : ap (@Wtil_rec A B f g C D Q cct' ppt') (ppt b y) = ppt' b y. Proof. unfold Wtil_rec. eapply (cancelL (transport_const (ppt (C:=C) b y) _)). refine ((apD_const (@Wtil_ind A B f g C D (fun _ => Q) cct' _) (ppt b y))^ @ _). refine (Wtil_ind_beta_ppt (fun _ => Q) _ _ _ _). Defined.
Require Import HoTT.Basics. Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe. Require Import HoTT.Colimits.Coeq.