proposition: Lemma term_of_aterm_sub : forall s k t, k > maxvar t -> term_of_aterm (sub s t) = apply_subst (sub_of_asub s k) (term_of_aterm t).
proof: Proof. intros s k t; pattern t; apply ATerm.term_ind with (Q := fun n (ts : aterms n) => k > maxvars ts -> terms_of_aterms (Vmap (sub s) ts) = map (apply_subst (sub_of_asub s k)) (terms_of_aterms ts)); clear t. simpl. intros. rewrite find_sub_of_asub. case_eq (bgt_nat k x); intros. refl. rewrite bgt_nat_ko in H0. lia. intros. simpl sub. rewrite !term_of_aterm_fun. simpl. f_equal. apply H. hyp. refl. intros t n ts. simpl. rewrite maxvars_cons, gt_max. intros. destruct H1. rewrite H. 2: hyp. rewrite H0. 2: hyp. refl. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution)