proposition: Lemma tree_to_echelon_prop2 t: tree_to_echelon (Tree_to_tree t) = Tree_to_echelon t.
proof: Proof. have H0 x: treep (Tree_to_tree x) by case: (Tree_to_tree_prop x). elim:t. - by move => n; rewrite (proj31 tree_to_echelon_E _ (nat_to_B_Nat n)) /=. - by move => e Hr; rewrite /= (proj32 tree_to_echelon_E _ (H0 e)) Hr. - move => e Hr1 e' Hr2. by rewrite /= (proj33 tree_to_echelon_E _ _ (H0 e) (H0 e')) Hr1 Hr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)