(P : Type) (scct' : forall a (x : C a), P) (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y)) : sWtil -> P := sWtil_ind (fun _ => P) scct' (fun b y => transport_const _ _ @ sppt' b y).
Require Import HoTT.Basics. Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe. Require Import HoTT.Colimits.Coeq.