proposition: Lemma is_a_pos_context : forall u c, is_a_pos (term_of_aterm (fill c u)) (pos_context c) = true.
proof: Proof. induction c; intros. refl. simpl fill. rewrite term_of_aterm_fun. simpl. rewrite terms_of_aterms_cast, terms_of_aterms_app. simpl. assert (nth_error (terms_of_aterms t ++ term_of_aterm (fill c u) :: terms_of_aterms t0) i = nth_error (terms_of_aterms t ++ term_of_aterm (fill c u) :: terms_of_aterms t0) (length (terms_of_aterms t))). f_equal. rewrite length_terms_of_aterms. refl. rewrite H, nth_error_at_pos. hyp. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution)