proposition: Lemma rpo_eq_subst : forall bb s t, rpo_eq bb s t -> forall sigma, rpo_eq bb (apply_subst sigma s) (apply_subst sigma t).
proof: Proof. intros bb s t H sigma; inversion H as [t1 t2 Heq | t1 t2 Hlt]; subst t1 t2. apply Equiv; apply equiv_subst; assumption. apply Lt; apply rpo_subst; assumption. 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)