proposition: Lemma rpo_mul_remove_equiv_aux1 : forall bb l l' s s', equiv s s' -> rpo_mul bb (s :: l) (s' :: l') -> rpo_mul bb l l'.
proof: Proof. intros. apply rpo_mul_remove_equiv_aux with s s'. intros H1 H2. apply rpo_antirefl. trivial. 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)