fact: Fixpoint height_t (t:tree) : nat := match t with | Null_t => O | Two_t tl _ tr => max (height_t tl) (height_t tr) | Three_t tl _ tm _ tr => max (max (height_t tl) (height_t tm)) (height_t tr) end.
imports: ExtLib.Structures.Monads ExtLib.Data.Monads.OptionMonad ExtLib.Programming.Extras