fact: Definition get (x : fvar) (e : env) : option sort := match find (fun p => if eq_nat_dec x (fst p) then true else false) e with | Some p => Some (snd p) | None => None end.
imports: Equations(Equations) Arith List ListSet Lia Program