proposition: Lemma nodup_lelistA_strict : forall B a S (mb : list B) (HL : nodup (a::mb)), lelistA (S%) a mb -> lelistA S a mb.
proof: Proof. intros. induction mb; intuition. simpl in *. inversion H; subst. apply cons_leA. destruct H1; subst; try tauto. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil) CoLoR(ListNodup)