proposition: Lemma rwr_at_pos : forall R p t sigma u v t', subterm_at_pos t p = Some (apply_subst sigma u) -> rwr R u v -> t' = (replace_at_pos t (apply_subst sigma v) p) -> rwr R t t'.
proof: Proof. intros R p; induction p as [ | i p]; intros t sigma u v t' Sbt H H'; simpl in Sbt. injection Sbt; clear Sbt; intros; subst; simpl. apply th_eq_closure; apply t_step; apply at_top; apply instance; trivial. destruct t as [x | f l]. discriminate. subst t'; simpl; apply general_context. revert l Sbt; induction i as [ | i]; intros [ | s l] Sbt; simpl. discriminate. simpl in Sbt. generalize (IHp s sigma u v _ Sbt H (eq_refl _)). generalize (replace_at_pos s (apply_subst sigma v) p); clear. intros t H; induction H as [t1 t2 H | t1 t2 t3 H1 H2]. do 2 left; assumption. right with (t2 :: l); [left | idtac]; assumption. discriminate. simpl in Sbt; generalize (IHi _ Sbt); clear. intro H; induction H as [l1 l2 H | l1 l2 l3 H1 H2]. left; right; assumption. apply trans_clos_is_trans with (s :: l2); trivial. left; right; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)