proposition: Theorem eqlistA_unique : forall (xs ys : list A) (p q : eqlistA R xs ys), p = q.
proof: Proof. induction p using eqlistA_ind'; uniqueness 2. Qed.
imports: Coq.Arith.Peano_dec Coq.Lists.SetoidList Lia Metalib.CoqUniquenessTac