fact: Definition option_rel {X : Type} (R : relation X) : relation (option X) := fun mx my => match mx,my with | Some x, Some y => R x y | None, None => True | _, _ => False end.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)