proposition: Lemma r_subset_dec : forall X Y, {r_subset X Y} + {~r_subset X Y}.
proof: Proof. move => X Y. case_eq (sim_incl X Y). move/sim_inclP => h. by left. move/sim_inclP => h. by right => h'; apply: h. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)