proposition: Lemma tree_value_prop E: [/\ (forall n, natp n -> tree_value E (Tb n) = Vg E n), (forall x, treep x -> tree_value E (Tp x) = \Po (tree_value E x))& (forall x y, treep x -> treep y -> tree_value E (Tx x y) = (tree_value E x) \times (tree_value E y))].
proof: Proof. rewrite /tree_value;split. - by move => n nN; rewrite tree_recdef_pb'. - by move => t tp ; rewrite tree_recdef_pp. - by move => t t' tp tp' ; rewrite tree_recdef_px. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)