proposition: Lemma dual_laws l (X: ops): laws (level.dual l) X -> laws l (dual X).
proof: Proof. intro H. constructor; try (destruct l; apply H). constructor. apply H. intros x y z H1 H2. revert H2 H1. simpl. apply H. intros x y. simpl. rewrite weq_spec. tauto. intro. simpl. eapply @capcup_. apply H. inverse_lower l Hl. intro. simpl. eapply @cupneg. apply H. inverse_lower l Hl. intro. simpl. eapply @capneg. apply H. inverse_lower l Hl. Qed.
imports: common level