proposition: Lemma sub_behead (T : eqType) x (xs ys : seq T) : {subset x :: xs <= ys} -> {subset xs <= ys}.
proof: Proof. move => sub a H. apply: sub. by rewrite inE H orbT. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)