proposition: Lemma sub_fresh_vars n (ts : terms n) : ts = Vmap (sub (sub_vars ts)) (fresh_vars n).
proof: Proof. apply Veq_nth. intros. rewrite Vnth_map, Vnth_fresh_vars. simpl. unfold sub_vars. rewrite val_of_vec_eq with (h:=ip). refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)