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