proposition: Lemma cong_equiv_inv (Δ : Tel) (T : Type) (f : Δ -> T) (u v : Δ) : IsEquiv f -> f u = f v -> u =={Δ} v.
proof: Proof. intros. induction Δ; simpl; simpl in *. + 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). + assert (u = v). transitivity (f ^-1 (f u)). symmetry. apply (eissect f u). transitivity (f ^-1 (f v)). now apply (Top.cong equiv_inv) in H. apply (eissect f v). apply (equiv_inv (f:=path_sigma_uncurried u v)) in H0. exists H0.1. set (f' := fun v2 : t0 v.1 => f &(v.1 & v2)). apply (X0 _ f'). apply axiom. subst f'. simpl. apply Top.cong. apply Top.cong. exact H0.2. Defined.
imports: Equations DepElimDec EqDecInstances