proposition: Lemma ctree_cons_pairs_partition t1 t2 t3 pt1 pt2 pt3 : ctree_partition t1 pt1 -> ctree_partition t2 pt2 -> ctree_partition t3 pt3 -> ctree_partition (CtreeNode t1 t2 t3) (ctree_cons_pairs pt1 pt2 pt3).
proof: Proof. move: pt1 pt2 pt3 => [t1' t1''] [t2' t2''] [t3' t3'']. rewrite ctree_cons_pairs_spec /= /ctree_mem => ppt1 ppt2 ppt3 et. by rewrite 2!ctree_sub_cons; case: et => [|[] et] /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)