fact: Fixpoint twothree_find {V} (k : K) (m : twothree V) : option V := match m with | Leaf => None | Two l k' v' r => match RD_K k k' with | Eq => Some v' | Lt => twothree_find k l | Gt => twothree_find k r end | Three l k1 v1 m k2 v2 r => match RD_K k k1 with | Eq => Some v1 | Lt => twothree_find k l | Gt => match RD_K k k2 with | Eq => Some v2 | Lt => twothree_find k m | Gt => twothree_find k r end end end.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Maps ExtLib.Structures.Monads ExtLib.Structures.Reducible