proposition: Theorem lelistA_unique : forall (x : A) (xs : list A) (p q : lelistA R x xs), p = q.
proof: Proof. induction p using lelistA_ind'; uniqueness 1. Qed.
imports: Coq.Arith.Peano_dec Coq.Lists.SetoidList Lia Metalib.CoqUniquenessTac