proposition: Lemma conv_compat' A B (x y: X A B): x` == y` -> x == y.
proof: Proof. intro H. rewrite <- (conv_invol x). rewrite <- (conv_invol y). apply conv_compat; exact H. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing)