{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 (y : C (f b)), cct' (f b) y = cct' (g b) (D b y)) : Wtil A B f g C D -> Q := Wtil_ind (fun _ => Q) cct' (fun b y => transport_const _ _ @ ppt' b y).
Require Import HoTT.Basics. Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe. Require Import HoTT.Colimits.Coeq.