proposition: Theorem empty_dec: {lang A i ≦ bot} + {~ (lang A i ≦ bot)}.
proof: Proof. case_eq empty; [left|right]. apply (empty_lang1 _ steps_refl H). intro E. apply empty_lang2 in E. rewrite H in E. discriminate. Qed.
imports: comparisons positives ordinal pair lset monoid boolean prop sups bmx