proposition: Lemma tree_to_echelon_E (f:=tree_to_echelon) : [/\ forall n, natp n -> f (Tb n) = Ech_base (csucc n), forall t, treep t -> f (Tp t) = Ech_powerset (f t) & forall t t', treep t -> treep t' -> f (Tx t t') = Ech_product (f t) (f t')].
proof: Proof. rewrite /f/tree_to_echelon; split. - by move => n nN;rewrite tree_recdef_pb'. - by move => x 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)