proposition: Lemma red_pos_ok : forall R t u, red R t u <-> red_pos R t u.
proof: Proof. split; intro. redtac. unfold red_pos. exists (pos_context c). exists l. exists r. exists s. intuition; rewrite xl. apply subterm_fill_pos_context. rewrite yr. apply replace_fill_pos_context. unfold red. unfold red_pos in H. decomp H. exists x0. exists x1. apply subterm_pos_elim in H1. destruct H1. destruct a. exists x3. exists x2. intuition. ded (replace_pos_elim H3). destruct X. destruct a. rewrite H in H2. inversion H2. subst x4. hyp. Qed.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)