proposition: Lemma ctr_decr_eq A lfk lf1 lf2 lf3 r : let cdecr_r e := cdecr e lf1 lf2 lf3 r in @ctr_decr A lfk lf1 lf2 lf3 r = lfk (cdecr_r Color1) (cdecr_r Color2) (cdecr_r Color3).
proof: Proof. rewrite /cdecr; elim: r => // bs t r IHr in lf1 lf2 lf3 *. by rewrite !ctr_decr_some IHr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)