proposition: Lemma mx_blocks_equal: forall (a a': MX x y) b b' c c' (d d': MX n m), mx_blocks a b c d == mx_blocks a' b' c' d' -> a==a' /\ b==b' /\ c==c' /\ d==d'.
proof: Proof. intros. rewrite <- (mx_block_11 a b c d) at 1. rewrite <- (mx_block_10 a b c d) at 1. rewrite <- (mx_block_01 a b c d) at 1. rewrite <- (mx_block_00 a b c d) at 1. rewrite H. rewrite mx_block_00, mx_block_01, mx_block_10, mx_block_11. repeat split; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)