{A} {a : A} {X : A -> Type} (e : forall (b : A), a = b <~> X b) (P : forall (b : A), X b -> Type) (r : P a (e a 1)) : forall (b : A) (x : X b), P b x. Proof. intro b. srapply (equiv_ind (e b)). intros []. exact r. Defined.
Require Import