Representing trees with functions (continued)

Consider the following inductive types for binary trees (with nodes labeled by integers).
Require Import ZArith.

Inductive Z_btree : Set :=
  Z_leaf : Z_btree | 
  Z_bnode : Z -> Z_btree -> Z_btree -> Z_btree.

Inductive Z_fbtree : Set :=
 | Z_fleaf : Z_fbtree 
 | Z_fnode : Z  -> (bool -> Z_fbtree) -> Z_fbtree.
Define functions :
f1 : Z_btree : Z_fbtree
f2 : Z_fbtree : Z_btree
that establish the most natural bijection between the two types.
Prove the following theorem:
Theorem f2_f1 : forall t: Z_btree, f2 (f1 t) = t.
What is missing to prove the following statement?
Theorem f1_f2 : forall t: Z_fbtree, f1 (f2 t) = t.

Solution

This file