(x : A') (h : forall y : B' x, IWPath (j' x y)) : IWPath_ind _ (iwpath_sup x h) = S x h (fun c => IWPath_ind _ (h c)). Proof. destruct x as [x [a b]]. cbv in h. refine (_ @ _). { refine (_ @ ap _ (eisadj (path_forall _ _) h)). refine (paths_ind _ (fun b p' => paths_ind _ (fun r p'' => P (i x ; (iw_sup I A B i j x a , r)) p'') (IWPath_ind_refl (i x) (iw_sup I A B i j x a)) _ (ap (iw_sup I A B i j x) p') = paths_rec (path_forall _ _ (apD10 p')) (fun p'' => P (_ ; (_, _)) (ap (iw_sup I A B i j x) p'')) (S (x ; (a, b)) (apD10 p') (fun c => IWPath_ind (_ ; (_, _)) (apD10 p' c))) p' (eissect apD10 p')) _ _ _). exact (transport_compose _ _ _ _)^. } by cbn; destruct (eisretr apD10 h). Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.