proposition: Lemma Vmap_fsub_fresh x0 n (ts : terms n) : Vmap (sub (fsub x0 ts)) (fresh (S x0) n) = ts.
proof: Proof. intros. apply Vmap_eq_nth. intros. rewrite Vnth_fresh. simpl. set (x := S(x0+i)). assert (h1 : x0<x). unfold x. lia. assert (h2 : x<=x0+n). unfold x. lia. assert (fsub x0 ts x = Vnth ts (lt_pm h1 h2)). apply fsub_nth. rewrite H. apply Vnth_eq. unfold x. lia. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)