proposition: Lemma tree6_1: [/\ Vg Tree6 \0c = Tree_to_tree (Tbase 0), Vg Tree6 \1c = Tree_to_tree (Tbase 1), Vg Tree6 \2c = Tree_to_tree (Tpowerset (Tbase 0)), Vg Tree6 \3c = Tree_to_tree (Tpowerset (Tpowerset (Tbase 0))) & Vg Tree6 \4c = Tree_to_tree (Tpowerset (Tbase 1)) /\ Vg Tree6 \5c = Tree_to_tree (Tproduct (Tpowerset (Tpowerset (Tbase 0))) (Tpowerset (Tbase 1)))].
proof: Proof. move: scheme_ex1_ok1 => [ha hb hc [v0 v1 v2 v3 [v4 v5]]]. move:(clt_6) => [lt06 lt16 lt26 lt36 [lt46 lt56]]. have V0: (Vg Tree6 \0c) = Tree_to_tree (Tbase 0). have ra: \0c <c slength (scheme_ex1) by rewrite hb. move: (ET_val1 ha ra); rewrite v0; aw => zz; move: (zz (erefl \0c)). move => [n [na ->]]. have: nat_to_B 1 = nat_to_B n.+1 by rewrite /= succ_zero na. move/nat_to_B_injective => /eqP; rewrite eqSS => /eqP <- //. have V1: Vg Tree6 \1c = Tree_to_tree (Tbase 1). have ra: \1c <c slength (scheme_ex1) by rewrite hb; exact:lt16. move: (ET_val1 ha ra); rewrite v1; 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 V2: (Vg Tree6 \2c) = Tree_to_tree (Tpowerset (Tbase 0)). have ra: \2c <c slength (scheme_ex1) 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 (Tpowerset (Tbase 0))). have ra: \3c <c slength (scheme_ex1) by rewrite hb. move: (ET_val2 ha ra); rewrite v3; aw => zz; move: (zz (erefl \0c)). move => [E ]; rewrite /Vl. by rewrite -/Tree6 /Vl cpred3 V2 => /Tree_to_tree_injective ->. have V4: (Vg Tree6 \4c) = Tree_to_tree (Tpowerset (Tbase 1)). have ra: \4c <c slength (scheme_ex1) by rewrite hb. move: (ET_val2 ha ra); rewrite v4; aw => zz; move: (zz (erefl \0c)). by move => [E]; rewrite /Vl cpred2 V1 => /Tree_to_tree_injective ->. have V5: (Vg Tree6 \5c) = Tree_to_tree (Tproduct(Tpowerset(Tpowerset (Tbase 0))) (Tpowerset (Tbase 1))). have ra: \5c <c slength (scheme_ex1) by rewrite hb. move: (ET_val3 ha ra); rewrite v5; aw => zz. move: (zz (@succ_nz \3c) (@succ_nz \4c)). rewrite -/Tree6 /Vl cpred4 cpred5 V3 V4; move=> [E [F []]]. move=> /Tree_to_tree_injective -> /Tree_to_tree_injective -> //. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)