proposition: Lemma ET_val2 c i (f := echelon_to_trees c): echelon c -> i <c (slength c) -> Q (Vg c i) = \0c -> exists2 E, Tree_to_tree E = (Vl f (P (Vg c i))) & Tree_to_tree (Tpowerset E) = Vg f i.
proof: Proof. move => ha hb az. move: (echelon_to_trees_prop ha) => [_ _ hd hc]. move: (hc _ hb) => [_ he2 _] {hc}; move: (he2 az) => [qa qb qc] {he2}. have mN:= (proj2 (proj1 (proj1 ha))). have iN:= (NS_lt_nat hb mN). set a := P (Vg c i). move: (cpred_pr6' iN qa qb) => [sa sb sc]. move: (Tree_to_tree_surjective (hd _(clt_ltT sc hb))) => [e ev]. by exists e => //; rewrite /f qc /= /Vl ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)