fact: Fixpoint vm_add (x: positive) (v : A) (m : t) {struct m} : t := match m with | Empty => singleton x v | Elt vl => match x with | xH => Elt v | xO p => Branch (singleton p v) vl Empty | xI p => Branch Empty vl (singleton p v) end | Branch l o r => match x with | xH => Branch l v r | xI p => Branch l o (vm_add p v r) | xO p => Branch (vm_add p v l) o r end end.
imports: ZArith_base List