`{IsEquiv A B f} (P : B -> Type) (df : forall x:A, P (f x)) (x : A) : equiv_ind f P df (f x) = df x. Proof. unfold equiv_ind. rewrite eisadj. rewrite <- transport_compose. exact (apD df (eissect f x)). Defined.
Require Import