proposition: Lemma eq_sym_equiv@{i} {A : Type@{i}} {x y : A} : Equiv@{i} (x = y) (y = x).
proof: Proof. unshelve refine {| equiv a := eq_sym a |}. unshelve refine {| equiv_inv a := eq_sym a |}. intro e; destruct e. apply eq_refl. intro e; destruct e. apply eq_refl. intro e; destruct e. apply eq_refl. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances