proposition: Lemma expr_leq_or_weq_correct b l n m (x y: expr n m): e_level x + e_level y ≪ l -> expr_leq_or_weq b x y -> @leq_or_weq b (expr_lattice_ops _ _ l _ _) x y.
proof: Proof. intros Hl H. destruct b. apply expr_leq_correct; assumption. apply eqb_eq in H as <-. reflexivity. Qed.
imports: kleene syntax powerfix