fact: Fixpoint pos_eq (m n:positive) {struct m} :bool := match m with xI mm => match n with xI nn => pos_eq mm nn | _ => false end | xO mm => match n with xO nn => pos_eq mm nn | _ => false end | xH => match n with xH => true | _ => false end end.
imports: List Bintree Bool BinPos