`{Funext} {A : Type} {B : A -> Type} (a : forall x, B x) (P : forall b, a == b -> Type) (f : P a (fun _ => 1%path)) {b : forall x, B x} (p : a == b) : P b p. Proof. refine (equiv_ind apD10 (P b) _ p). intros []. exact f. Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.