(x : A) (a : forall c : B x, IW I A B i j (j x c)) : iwpath_sup (x; (a, a)) (apD10 1) = idpath. Proof. unfold iwpath_sup. rewrite path_forall_1. reflexivity. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.