proposition: Lemma Vbreak_fresh p : forall n k, Vbreak (fresh k (n+p)) = (fresh k n, fresh (k+n) p).
proof: Proof. induction n; simpl; intros. rewrite Nat.add_0_r. refl. rewrite IHn. simpl. rewrite Nat.add_succ_r. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)