proposition: Lemma dualize {h} {P: ops -> Prop} (L: forall l X, laws l X -> h ≪ l -> P X) {l X} {H: laws l X} {Hl:level.dual h ≪ l}: P (dual X).
proof: Proof. apply L with (level.dual l). apply dual_laws. destruct l; apply H. revert Hl. rewrite 2lower_spec. destruct l; destruct h; simpl. tauto. Qed.
imports: common level