fact: Definition asNth {ts : pmap Type} (p : positive) (oe : OneOf ts) : option (match pmap_lookup' ts p with | None => Empty_set | Some T => T end) := @asNth' ts p oe.(index ts) oe.(value ts).
imports: Coq(PArith) ExtLib.Data.Map.FMapPositive ExtLib.Data.Eq ExtLib.Tactics.Injection Coq(PArith)