proposition: Lemma ctree_leaf_pair_spec lf1 lf2 lf3 lf1' lf2' lf3' : let if_e lf lf' := if ctree_empty lf' then lf else CtreeEmpty in let t' := ctree_cons lf1' lf2' lf3' in let t'' := ctree_cons (if_e lf1 lf1') (if_e lf2 lf2') (if_e lf3 lf3') in ctree_leaf_pair lf1 lf2 lf3 lf1' lf2' lf3' = CtreePair t' t''.
proof: Proof. by case: lf1'; case: lf2'; case: lf3'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)