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