proposition: Lemma replace_fill_pos_context : forall c u v, replace_pos (fill c u) (pos_context c) v = Some (fill c v).
proof: Proof. induction c; intros; simpl. destruct u; auto. case (lt_ge_dec i (arity f)); intro. rewrite Vnth_cast. rewrite Vnth_app_cons. 2: lia. rewrite (IHc u v). f_equal. apply args_eq. apply Veq_nth; intros. rewrite Vnth_cast. destruct (eq_nat_dec i i0). subst i0. rewrite Vnth_replace. rewrite Vnth_app_cons. refl. rewrite Vnth_replace_neq. 2: hyp. rewrite Vnth_cast. apply Vnth_app_cons_neq. auto. Qed.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)