proposition: Lemma permut0_rpo_mul_antirefl: forall l1 l2 rpo_infos, permut0 equiv l1 l2 -> rpo_mul (bb rpo_infos) l1 l2 -> False.
proof: Proof. induction l1. induction l2. intros. apply rpo_mul_antirefl with rpo_infos []. trivial. intros. inversion H. induction l2. intros. inversion H. apply app_eq_nil in H3. destruct H3. discriminate. intros. inversion H0. apply (rpo_mul_antirefl rpo_infos (l:=a::l1)). eapply List_mul. apply H1. apply permut0_trans with (a0::l2). apply equiv_equiv. trivial. apply H2. trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)