fact: Fixpoint locateGreatest (t:tree) (c:context) : option (E * (context + E * context)) := match t with | Null_t => None | Two_t tl em tr => liftM sum_tot $ locateGreatest tr (TwoRightHole_c tl em c) <+> ret (em, inl c) | Three_t tl el tm er tr => liftM sum_tot $ locateGreatest tr (ThreeRightHole_c tl el tm er c) <+> ret (er, inr (el, c)) end.
imports: ExtLib.Structures.Monads ExtLib.Data.Monads.OptionMonad ExtLib.Programming.Extras