fact: Fixpoint Z_btree_rect (f:Z_btree->Type)(exp1:f Z_leaf) (exp2:forall (n:Z)(t1:Z_btree), f t1 -> forall t2:Z_btree, f t2 -> f (Z_bnode n t1 t2)) (t:Z_btree) : f t := match t as x return f x with | Z_leaf => exp1 | Z_bnode n t1 t2 => exp2 n t1 (Z_btree_rect f exp1 exp2 t1) t2 (Z_btree_rect f exp1 exp2 t2) end.
imports: ZArith List Arith Zwf Relations Inverse_Image