fact: Definition isJust {a} (x : Maybe a) := if x then true else false.
imports: Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Semigroup Category.Theory.Coq.Monoid Category.Theory.Coq.Traversable