proposition: Lemma mx_blocks_zero x y n m: 0 == @mx_blocks _ A x y n m 0 0 0 0.
proof: Proof. simpl. intros. destruct_blocks; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)