proposition: Lemma fold_right_pair_NoDup : forall l r (Hl: NoDupA (eqk (elt:=oee')) l) (Hl: NoDupA (eqk (elt:=oee')) r), NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) r l).
proof: Proof. induction l; simpl; auto. destruct a; simpl; auto. inversion_clear 1. intros; apply add_NoDup; auto. Qed.
imports: FMapInterface