fact: Fixpoint remove (i : key) (m : t A) : t A := match i with | xH => match m with | Leaf => Leaf | Node Leaf _ Leaf => Leaf | Node l _ r => Node l None r end | xO ii => match m with | Leaf => Leaf | Node l None Leaf => match remove ii l with | Leaf => Leaf | mm => Node mm None Leaf end | Node l o r => Node (remove ii l) o r end | xI ii => match m with | Leaf => Leaf | Node Leaf None r => match remove ii r with | Leaf => Leaf | mm => Node Leaf None mm end | Node l o r => Node l o (remove ii r) end end.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface