proposition: Lemma memc0_ttail et : (Color0 \in ttail et) = ~~ proper_trace et || (Color0 \in et).
proof: Proof. by case: et => [|[] et]; rewrite /ttail //= memc0_permt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)