fact: Definition Into {ts} {T : Type} (n : positive) (pf : pmap_lookup' ts n = Some T) : T -> OneOf ts := match pf in _ = X return match X with | Some T => T | None => Empty_set end -> OneOf ts with | eq_refl => @mkOneOf ts n end.
imports: Coq(PArith) ExtLib.Data.Map.FMapPositive ExtLib.Data.Eq ExtLib.Tactics.Injection Coq(PArith)