proposition: Lemma has_matchP bs (ct : spec_ctree) w : reflect (exists2 et, ct et & matchpg bs et w) (has_match bs ct w).
proof: Proof. elim: w => [|s w IHw] /= in bs ct *. by apply: (iffP idP) => [|[[] //]]; exists [::]. case Ds: s; rewrite /= -/colseq. - case: (IHw) => [wMe2 | not_wMe2]. by left; have [et] := wMe2; exists (Color2 :: et). apply: (iffP (IHw _ _)) => [[et] | []]; first by exists (Color3 :: et). by case=> [|[] et *] //; first case: not_wMe2; exists et. - apply: (iffP (IHw _ _)) => [[et] | []]; first by exists (Color1 :: et). by case=> [|[]] // et *; exists et. - case: bs => [|bs|bs]; first by right=> [] [] [|[]]. + apply: (iffP (IHw _ _)) => [[et] | []]; first by exists (Color2 :: et). by case=> [|[]] // et *; exists et. apply: (iffP (IHw _ _)) => [[et] | []]; first by exists (Color3 :: et). by case=> [|[]] // et *; exists et. case: bs => [|bs|bs]; first by right=> [] [] [|[]]. + apply: (iffP (IHw _ _)) => [[et] | []]; first by exists (Color3 :: et). by case=> [|[]] // et *; exists et. apply: (iffP (IHw _ _)) => [[et] | []]; first by exists (Color2 :: et). by case=> [|[]] // et *; exists et. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)