proposition: Lemma solution {A} (t : A) : tele ( x : A ) in (x = t) <~> [].
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 _ _). constructor. Defined.
imports: Equations DepElimDec