proposition: Lemma cong_equiv_inv@{i} (Δ : Tel@{i}) (T : Type@{i}) (f : Δ -> T) (u v : Δ) : IsEquiv f -> f u = f v -> u =={Δ} v.
proof: Proof. intros. apply eq_points_equiv. apply (Top.cong equiv_inv) in H. transitivity (f ^-1 (f u)). symmetry. apply (eissect f u). transitivity (f ^-1 (f v)). apply H. apply (eissect f v). Defined.
imports: Equations Utf8 DepElimDec EqDecInstances