proposition: Lemma Echelon_value_ex2 E (A := Vg E \0c): echelon_of_base Echelon_ex2 E = \Po ((A \times A) \times A) /\ echelon_can_extension Echelon_ex2 E = \Pof ((A \ftimes A) \ftimes A).
proof: Proof. move:(proj1 Tree_ex2_prop ) => xx. move:(tree_value_prop E) => [ha hb hc]. move:(tree_extension_prop E) => [ha' hb' hc']. move: (tdepth_prop_inv) => [qa qb qc]. move: (proj1 (qa _ NS0)) => ta. move: (proj1 (qc _ _ ta ta)) => tb. move: (proj1 (qc _ _ tb ta)) => tc. rewrite /Echelon_ex2 (echelon_of_base_of_tree E xx) /Tree_ex2. rewrite (hb _ tc) (hc _ _ tb ta) (hc _ _ ta ta) (ha _ NS0). rewrite (can_extension_of_tree E xx). by rewrite (hb' _ tc) (hc' _ _ tb ta) (hc' _ _ ta ta) (ha' _ NS0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)