proposition: Lemma rpo_eq_add_context : forall bb p ctx s t, rpo_eq bb s t -> is_a_pos ctx p = true -> rpo_eq bb (replace_at_pos ctx s p) (replace_at_pos ctx t p).
proof: Proof. intros bb p ctx s t H P; inversion H; clear H; subst. apply Equiv; apply equiv_add_context; assumption. apply Lt; apply rpo_add_context; 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)