proposition: Lemma NoConfusionPackage_isequiv {A} (a b : A) {e : NoConfusionPackage A} : Equiv (a = b) (NoConfusion a b).
proof: Proof. unshelve refine {| equiv := noConfusion |}. unshelve refine {| equiv_inv := noConfusion_inv |}. red; intros. apply axiom_triangle. red. apply noConfusion_is_equiv. apply axiom_triangle. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances