proposition: Corollary lang_incl_dec A B: vars A ≦ vars B -> forall i j, {lang A i ≦ lang B j} + {~(lang A i ≦ lang B j)}.
proof: Proof. intros. eapply sumbool_iff. symmetry. now apply diff_spec. apply empty_dec. Qed.
imports: comparisons positives ordinal pair lset monoid boolean prop sups bmx