proposition: Lemma noduplicates_length_eq : forall l1 l2, noduplicates l1 -> noduplicates l2 -> (forall x, mem x l1 <-> mem x l2) -> length l1 = length l2.
proof: Proof. Proof using. introv H1 H2 EQ. forwards~: noduplicates_length_le l1 l2. { intros. rewrite~ <- EQ. } forwards~: noduplicates_length_le l2 l1. { intros. rewrite~ EQ. } math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)