proposition: Lemma Vnth_fresh : forall n i (h : i < n) x0, Vnth (fresh x0 n) h = Var (x0+i).
proof: Proof. induction n; simpl. intros. absurd (i<0); lia. intro. destruct i. auto. intros. assert (x0+S i=(S x0)+i). lia. rewrite H. apply IHn. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)