proposition: Lemma tree_extension_prop f: [/\ (forall n, natp n -> tree_extension f (Tb n) = Vg f n), (forall x, treep x -> tree_extension f (Tp x) = \Pof (tree_extension f x))& (forall x y, treep x -> treep y -> tree_extension f (Tx x y) = (tree_extension f x) \ftimes (tree_extension f y))].
proof: Proof. rewrite /tree_extension;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)