fact: Definition Wtil_rec_beta_ppt {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.
imports: HoTT.Basics Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe HoTT.Colimits.Coeq