proposition: Lemma mx_blocks_plus x y n m: forall M M' N N' P P' Q Q', mx_blocks M N P Q + mx_blocks M' N' P' Q' == @mx_blocks _ A x y n m (M+M') (N+N') (P+P') (Q+Q').
proof: Proof. simpl. intros. destruct_blocks; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)