Lvc.Infra.LeastFresh

Require Import CSet Le Arith.Compare_dec.
Require Import Plus Util Map Get Take LengthEq SafeFirst.
Require Export PidgeonHole StableFresh OrderedTypeMax.

Set Implicit Arguments.

Class LeastFresh V `{OrderedType V} :=
  {
    least_fresh :> set V → V;
    least_fresh_spec : ∀ G, least_fresh G ∉ G;
    least_fresh_least : ∀ G y, _lt y (least_fresh G) → y ∈ G;
    least_fresh_ext : ∀ G G', G [=] G' → least_fresh G = least_fresh G'
  }.

Arguments LeastFresh V {H}.