IW'_ind_beta_iw_sup' (P : forall i, IW' i -> Type) (S : forall x y, (forall c, P _ (y c)) -> P _ (iw_sup' x y)) x y : IW'_ind P S _ (iw_sup' x y) = S x y (fun c => IW'_ind P S _ (y c)) := idpath.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.