proposition: Lemma subterm_fill_pos_context : forall c u, subterm_pos (fill c u) (pos_context c) = Some u.
proof: Proof. induction c; intros; simpl. destruct u; auto. case (lt_ge_dec i (arity f)); intro. 2: lia. rewrite Vnth_cast. rewrite Vnth_app_cons. apply IHc. Qed.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)