proposition: Lemma solution@{i} {A : Type@{i}} (t : A) : Equiv@{i} (sigma@{i} A (fun x : A => x = t)) unit.
proof: Proof. refine {| equiv a := tt |}. unshelve refine {| equiv_inv e := telei t in eq_refl |}. - red; intros. destruct x. reflexivity. - red; intros. destruct x. now destruct pr2. - intros [x eq]. revert t eq. refine (Top.J@{i i} _ _). constructor. Defined.
imports: Equations Utf8 DepElimDec