proposition: Lemma ctree_proper_sel h t e : ctree_proper h t -> ctree_proper h.-1 (ctree_sel t e).
proof: Proof. by case: h t e => [|h] [t1 t2 t3|lf|] //= [] []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)