proposition: Lemma empty_lang2: lang A i ≦ bot -> empty.
proof: Proof. intro H. setoid_rewrite is_true_inf. intros j _. rewrite le_bool_spec. intro Hj. apply steps_least in Hj as [w [Hw ->]]. generalize i (H w) Hw. clear. induction w; intros i Hi Hw. simpl in *. destruct (v A i). now elim Hi. reflexivity. apply IHw. intro H. elim Hi. split. apply Hw. now left. assumption. intros ? ?. apply Hw. now right. Qed.
imports: comparisons positives ordinal pair lset monoid boolean prop sups bmx