forall l a, P (l ; (a, a)) idpath. Proof. rapply (IW_rect I A B i j (fun l a => P (l; (a, a)) idpath)). intros x a q. pose (S (x; (a, a)) _ q) as p. unfold iwpath_sup in p. refine (transport (P (i x; (iw_sup I A B i j x a, iw_sup I A B i j x a))) _ p). change (ap (iw_sup I A B i j x) (path_forall a a (apD10 idpath)) = ap (iw_sup I A B i j x) 1%path). refine (ap _ _). apply eissect. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.