proposition: Lemma ctree_mem_rotl t et : ctree_mem (ctree_rotl t) et = ctree_mem t (permt Eperm312 et).
proof: Proof. rewrite /ctree_mem; elim: et t => [|e et IHet] [t1 t2 t3|lf|] //=; by rewrite ctree_sub_cons //; case: e => /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)