{A B : Type} {P : A -> A -> Type} (e : B <~> A) (K : forall b0 b1 : B, P (e b0) (e b1) <~> b0 = b1) : forall a0 a1 : A, P a0 a1 <~> a0 = a1. Proof. equiv_intros e b0 b1. nrefine (_ oE K b0 b1). apply equiv_ap'. Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.