fact: Definition Union_Format {m} (formats : Vector.t (FormatM S T) m) : FormatM S T := fun s env tenv' => exists idx, Vector.nth formats idx s env ∋ tenv'.
imports: Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.Narcissus.Common.Specs Coq.Sets.Ensembles