proposition: Lemma tree6_2: echelon_to_tree scheme_ex1 = echelon_to_tree scheme_ex2.
proof: Proof. move: scheme_ex2_ok1 => [ha hb hc [v0 v1 v2 v3 [v4 v5]]]. move: scheme_ex1_ok1 => [_ hb' _ _]. suff: (Vg Tree6' \5c) = (Vg Tree6 \5c). by rewrite /echelon_to_tree /Vl hb hb' (cpred_pr1 (CS_nat NS5)). move: tree6_1 => [_ _ _ _ [ _ ->]]. move:(clt_6) => [lt06 lt16 lt26 lt36 [lt46 lt56]]. have V0: (Vg Tree6' \0c) = Tree_to_tree (Tbase 1). have ra: \0c <c slength (scheme_ex2) by rewrite hb. move: (ET_val1 ha ra); rewrite v0; aw => zz; move: (zz (erefl \0c)). move => [n [na ->]]. have: nat_to_B 2 = nat_to_B n.+1 by rewrite /= succ_zero succ_one na. by move/nat_to_B_injective => /eqP; rewrite eqSS => /eqP <- //. have V1: (Vg Tree6' \1c) = Tree_to_tree (Tbase 0). have ra: \1c <c slength (scheme_ex2) by rewrite hb. move: (ET_val1 ha ra); rewrite v1; aw => zz; move: (zz (erefl \0c)). move => [n [na ->]]. have: nat_to_B 1 = nat_to_B n.+1 by rewrite /= succ_zero na. by move/nat_to_B_injective => /eqP; rewrite eqSS => /eqP <- //. have V2: (Vg Tree6' \2c) = Tree_to_tree (Tpowerset (Tbase 1)). have ra: \2c <c slength (scheme_ex2) by rewrite hb. move: (ET_val2 ha ra); rewrite v2; aw => zz; move: (zz (erefl \0c)). by move => [E]; rewrite /Vl cpred1 V0 => /Tree_to_tree_injective ->. have V3: (Vg Tree6' \3c) = Tree_to_tree (Tpowerset (Tbase 0)). have ra: \3c <c slength (scheme_ex2) by rewrite hb. move: (ET_val2 ha ra); rewrite v3; aw => zz; move: (zz (erefl \0c)). move => [E ]; rewrite /Vl. by rewrite -/Tree6 /Vl cpred2 V1 => /Tree_to_tree_injective ->. have V4: (Vg Tree6' \4c) = Tree_to_tree (Tpowerset (Tpowerset (Tbase 0))). have ww: (cpred \4c) = \3c by rewrite (cpred_pr1 (CS_nat NS3)). have ra: \4c <c slength (scheme_ex2) by rewrite hb. move: (ET_val2 ha ra); rewrite v4; aw => zz; move: (zz (erefl \0c)). by move => [E]; rewrite /Vl ww V3 => /Tree_to_tree_injective ->. have ra: \5c <c slength (scheme_ex2) by rewrite hb. move: (ET_val3 ha ra); rewrite v5; aw => zz. move: (zz (@succ_nz \4c) (@succ_nz \2c)). rewrite -/Tree6 /Vl cpred3 cpred5 V2 V4; move=> [E [F []]]. move=> /Tree_to_tree_injective -> /Tree_to_tree_injective -> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)