proposition: Lemma subterm_pos_sub : forall s u p t, subterm_pos t p = Some u -> subterm_pos (sub s t) p = Some (sub s u).
proof: Proof. induction p; destruct t; simpl; intros. inversion H. simpl. destruct (s n); refl. inversion H. rewrite sub_fun. refl. discr. revert H. destruct (lt_ge_dec a (arity f)); intro. rewrite Vnth_map. apply IHp. hyp. discr. Qed.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)