(I : Type) (A : Type) (B : A -> Type) (i : A -> I) (j : forall x, B x -> I) : I -> Type := | iw_sup (x : A) : (forall (y : B x), I A B i j (j x y)) -> I A B i j (i x).
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.