proposition: Lemma ctree_sub0_cons_pairs pt1 pt2 pt3 et : let cp0 pt := ctree_pair_sub pt false in ctree_sub (cp0 (ctree_cons_pairs pt1 pt2 pt3)) et = ctree_sub (CtreeNode (cp0 pt1) (cp0 pt2) (cp0 pt3)) et.
proof: Proof. move: pt1 pt2 pt3 => [t1 t1'] [t2 t2'] [t3 t3']. by rewrite ctree_cons_pairs_spec /= ctree_sub_cons; case: et. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)