proposition: Lemma ap_equiv_inv@{i} (Δ : Type@{i}) (T : Type@{i}) (f : Δ -> T) (x y : Δ) : IsEquiv f -> f x = f y -> x = y.
proof: Proof. intros H. refine (fun q => (eissect f x)^ @ ap f^^-1 q @ eissect f y). Defined.
imports: Equations(Equations)