proposition: Theorem f1_f2 : forall t: Z_fbtree, f1 (f2 t) = t.
proof: Proof. induction t; simpl; auto. - do 2 rewrite H. unfold Zf_mknode. rewrite <- (extensionality _ _ (fun b:bool => if b then z0 true else z0 false) z0). + trivial. + destruct a; simpl; trivial. Qed.
imports: ZArith