proposition: Lemma QNoDup_CNoDup_Qap(l: list Q): QNoDup l IFF CNoDup Qap l.
proof: Proof. Proof with auto. induction l; simpl; split; intro... apply NoDup_nil. split. apply IHl. inversion_clear H... apply (CForall_prop _). intros ? A. inversion_clear H. intro E. apply H0. rewrite E. apply in_map... apply NoDup_cons. 2: firstorder. intro. destruct (proj1 (in_map_iff _ _ _) H) as [x [H0 H1]]. destruct X. apply (snd (@CForall_prop Q (Qap a) l) c0 x)... rewrite <- (Qred_correct x). rewrite H0. symmetry. apply Qred_correct. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q