proposition: Lemma 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).
proof: Proof. intro p; induction p as [ | i p ]; intros ctx s t R H; trivial; destruct ctx as [ v | f l ]. discriminate. assert (Status : forall g, g = f -> status g = status f). intros; subst; trivial. do 2 (rewrite replace_at_pos_unfold); destruct (status f); generalize (Status f (refl_equal _)); clear Status; intro Status. apply Top_eq_lex; trivial. generalize l i H; clear l i H; induction l as [ | u1 l ]; intros i H. destruct i; discriminate. destruct i; simpl in H; simpl. apply List_gt; trivial; apply IHp; trivial. apply List_eq; apply IHl; trivial. intros s' In_s'; assert (H' : exists t', In t' (replace_at_pos_list l t i p) /\ rpo_eq s' t'). generalize l i H In_s'; clear l i H In_s'; induction l as [ | u1 l ]; intros i H In_s'. destruct i; discriminate. destruct i; elim In_s'; clear In_s'; intro In_s'; subst. exists (replace_at_pos u1 t p); split; [ left | apply Lt; apply IHp ]; trivial. exists s'; split; [ right; trivial | apply Eq ]. exists s'; split; [ left; trivial | apply Eq ]. elim (IHl i H In_s'); intros t' [H1 H2]; exists t'; split; [ right | idtac ]; trivial. elim H'; clear H'; intros t' [H1 H2]; apply Subterm with t'; trivial. apply Top_eq_mul; trivial. assert (H' : exists l1, exists ui, exists l2, l = l1 ++ ui :: l2 /\ length l1 = i). generalize i H; clear i H; induction l as [ | u1 l ]; intros i H. destruct i; discriminate. destruct i as [ | i ]. exists (nil (A:= term)); exists u1; exists l; split; trivial. elim (IHl i H); intros l1 [ ui [ l2 [ H1 H2]]]. exists (u1 :: l1); exists ui; exists l2; split; subst; trivial. elim H'; clear H'; intros l1 [ ui [ l2 [ H1 H' ]]]; subst l. do 2 (rewrite replace_at_pos_list_replace_at_pos_in_subterm; trivial). apply (List_mul (replace_at_pos ui t p) nil (replace_at_pos ui s p :: nil) (l1 ++ l2)). simpl; apply list_permut_sym; apply list_permut_add_cons_inside; apply list_permut_refl. simpl; apply list_permut_sym; apply list_permut_add_cons_inside; apply list_permut_refl. intros b In_b; elim In_b; clear In_b; intro In_b; subst. exists (replace_at_pos ui t p); split; [ left | apply IHp ]; trivial. induction l1 as [ | u1 l1 ]; trivial; apply IHl1; trivial. contradiction. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term