proposition: Lemma in_freshl x : forall n x0, ~In x (freshl x0 n) -> x < x0 \/ x >= x0 + n.
proof: Proof. induction n; simpl; intuition. lia. ded (IHn (S x0) H1). lia. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)