fact: Definition fmap_poption@{} (x : poption@{i} T) : poption@{j} U := match x with | pNone => pNone@{j} | pSome x => pSome@{j} (f x) end.
imports: ExtLib.Structures.Functor ExtLib.Structures.Applicative ExtLib.Tactics.Injection