proposition: Lemma subterm_pos_elim : forall p t u, subterm_pos t p = Some u -> {C | context_pos t p = Some C /\ t = fill C u}.
proof: Proof. induction p; simpl; intros. exists Hole. simpl. destruct t; inversion H; auto. destruct t. discr. revert H. simpl. destruct (lt_ge_dec a (arity f)); intros. 2: discr. destruct (IHp _ _ H). destruct a0. rewrite H0. exists (Cont f (Veq_app_cons_aux3 l) (Vsub t (Veq_app_cons_aux1 l)) x (Vsub t (Veq_app_cons_aux2 l))). intuition. simpl. apply args_eq. rewrite <- H1. apply Veq_app_cons_aux. Defined.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)