fact: Definition NameTagAsStringOption {av T} (nt: NameTag av T) := match nt with | NTNone => None | NTSome key H => Some key end.
imports: Coq.Strings.String Computation.Core ADTRefinement Bedrock.Platform.Facade.DFacade Bedrock.Platform.Cito.StringMap