proposition: Lemma subterm_pos_replace_eq_Some : forall p u v t, subterm_pos t p = Some u -> {w | replace_pos t p v = Some w}.
proof: Proof. induction p; simpl; intros. destruct t; exists v; simpl; refl. destruct t. discr. simpl. case_eq (lt_ge_dec a (arity f)); intros l H0; rewrite H0 in H; clear H0. destruct (IHp _ v _ H). rewrite e. exists (Fun f (Vreplace t l x)). refl. discr. Defined.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)