proposition: Lemma tree_recdef_stable E: (forall n, natp n -> inc (h1 n) E) -> (forall x, inc x E -> inc (h2 x) E) -> (forall x x', inc x E -> inc x' E -> inc (h3 x x') E) -> (forall x, treep x -> inc (tree_rec x) E).
proof: Proof. move => ha hb hc. apply: tree_ind. - by move => n nN; rewrite tree_recdef_pb' //; apply: ha. - by move => x xt; rewrite tree_recdef_pp //; apply: hb. - move => x y xt yt; rewrite tree_recdef_px //; apply: hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)