fact: Axiom rpo_add_context : forall p ctx s t, rpo s t -> is_a_pos ctx p = true -> rpo (replace_at_pos ctx s p) (replace_at_pos ctx t p).
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term