fact: Parameter equiv_rpo_equiv_2 : forall bb t t', equiv t t' -> (forall s, rpo bb t s <-> rpo bb t' s).
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)