proposition: Lemma Tree_to_tree_surjective x: treep x -> exists e, x = Tree_to_tree e.
proof: Proof. move:x;apply: tree_ind. - move => n nN; move:(nat_to_B_surjective nN) => [k ->]. by exists (Tbase k). - by move => x _ [e ->]; exists (Tpowerset e). by move => x x' _ _ [e ->] [e' ->]; exists (Tproduct e e'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)