proposition: Lemma equiv_rpo_equiv_3 : forall bb t t', equiv t t' -> (forall s, rpo_eq bb s t <-> rpo_eq bb s t').
proof: Proof. intro bb. assert (H: forall t t', equiv t t' -> (forall s, rpo_eq bb s t -> rpo_eq bb s t')). intros t t' t_eq_t' s s_le_t; inversion s_le_t; subst. apply Equiv; transitivity t; trivial. apply Lt; rewrite <- (equiv_rpo_equiv_1 _ t_eq_t'); trivial. intros t t' t_eq_t' s; split; apply H; trivial. symmetry; 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)