proposition: Lemma diff_spec: vars A ≦ vars B -> forall i j, lang A i ≦ lang B j <-> lang diff (pair.mk i j) ≦ bot.
proof: Proof. intro H. cut (forall w i j, lang A i w ≦ lang B j w <-> ~ lang diff (pair.mk i j) w). intros G i j. split. intros Hij w Hw. apply G in Hw as []. apply Hij. intros Hij w. apply G. intro Hw. elim (Hij _ Hw). induction w; intros i j; simpl lang; rewrite pair.pi1mk, pair.pi2mk. case (v A i); case (v B j); firstorder discriminate. split. intros Hij [HaB Hw]. apply IHw in Hw as []. intro Aw. apply Hij. now split. intros Hw [Ha Aw]. split. apply H, Ha. eapply IHw. 2: eassumption. tauto. Qed.
imports: comparisons positives ordinal pair lset monoid boolean prop sups bmx