proposition: Lemma term_of_aterm_fill : forall u t c, term_of_aterm (fill c t) = replace_at_pos (term_of_aterm (fill c u)) (term_of_aterm t) (pos_context c).
proof: Proof. induction c; intros. refl. simpl fill. simpl pos_context. rewrite !term_of_aterm_fun, replace_at_pos_unfold. f_equal. rewrite !terms_of_aterms_cast, !terms_of_aterms_app. simpl. rewrite replace_at_pos_list_replace_at_pos_in_subterm, <- IHc. refl. rewrite length_terms_of_aterms. refl. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution)