proposition: Lemma ctree_union_proper h tl tr : ctree_proper h tl -> ctree_proper h tr -> ctree_proper h (ctree_union tl tr).
proof: Proof. elim: h => [|h IHh] in tl tr *; first by case: tl => //; case: tr. case: tl => // [tl1 tl2 tl3|]; case: tr => //= tr1 tr2 tr3 [? ? ? ?] [*]. by apply: ctree_cons_proper; apply: IHh. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)