proposition: Lemma ra b `{L: laws} f' (f: positive -> Pack X f') n m (x y: expr _ _ n m) (Hl: e_level x + e_level y ≪ l): expr_leq_or_weq b (norm true x) (norm true y) = true -> packed_eval f x <=[b]= packed_eval f y.
proof: Proof. intro H. apply (ra_normalise true b). assumption. intros x' y'. subst x' y'. eapply expr_leq_or_weq_correct in H. destruct b; apply (H _ L). now rewrite 2norm_level. Qed.
imports: kleene syntax powerfix