iw_sup' (x : A) (y : forall z : B x, IW' (j x z)) : IW' (i x) := (w_sup A B x (fun a => pr1 (y a)); (idpath, (fun a => pr2 (y a)))).
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.