(P : forall i, IW' i -> Type) (S : forall x y, (forall c, P _ (y c)) -> P _ (iw_sup' x y)) : forall x w, P x w. Proof. intros x [w r]. revert w x r. induction w as [a b k]. intros x [p IH]. destruct p. refine (S a (fun c => (b c; IH c)) _). intros c. apply k. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.