proposition: Theorem rpo_mul_antirefl : forall rpo_infos l, rpo_mul (bb rpo_infos) l l -> False.
proof: Proof. induction l. intros. inversion H. inversion H1. intros. apply IHl. apply rpo_mul_remove_equiv_aux1 with a a. reflexivity. 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)