proposition: Lemma lower_lattice_laws {h k} {X} {H: laws h X} {le: k ≪ h}: laws k X.
proof: Proof. constructor; try solve [ apply H | intro; apply H; eauto using lower_trans ]. intro. right. eapply @leq_bx. apply H. eauto using lower_trans. intro. right. eapply @leq_xt. apply H. eauto using lower_trans. Qed.
imports: common level