proposition: Lemma osl_R_pos : forall R f l1 l2, one_step_list R l1 l2 -> exists p, exists s, exists t, R s t /\ M.is_a_pos (M.Term f l1) (p::nil) = true /\ M.Term f l1 = M.replace_at_pos (M.Term f l1) s (p::nil) /\ M.Term f l2 = M.replace_at_pos (M.Term f l1) t (p::nil).
proof: Proof. intros R f l1 l2 H; revert l2 H; induction l1; intros l2 H; inversion H; subst; [ exists O; exists a; exists t2; repeat split; assumption |]; apply IHl1 in H3; destruct H3 as [p [s [t [H0 [H1 [H2 H3]]]]]]; exists (S p); exists s; exists t; repeat split; try assumption; [ simpl in H2; injection H2 | simpl in H3; injection H3 ]; intros Heq; simpl; rewrite <- Heq; reflexivity. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)