proposition: Lemma fresh_plus : forall n1 n2 x0, fresh x0 (n1+n2) = Vapp (fresh x0 n1) (fresh (x0+n1) n2).
proof: Proof. induction n1; simpl; intros. rewrite Nat.add_0_r. refl. apply Vtail_eq. rewrite IHn1. assert (S x0 + n1 = x0 + S n1). lia. rewrite H. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)