{A B I i j} (l : I) (w : IW I A B i j l) : forall (y : B (iw_label w)), IW I A B i j (j (iw_label w) y) := match w with | iw_sup x y => y end.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.