proposition: Lemma NoDupA_incl {A} (R R':relation A) : (forall x y, R x y -> R' x y) -> forall l, NoDupA R' l -> NoDupA R l.
proof: Proof. intros Incl. induction 1 as [ | a l E _ IH ]; constructor; auto. contradict E. revert E. rewrite 2 InA_alt. firstorder. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)