proposition: Lemma add_continuation_1 A0 A1 A2 (l1: X A0 A1) (l2: X A1 A2) (r: X A0 A2): l1*l2 == r -> forall B (q: X B A0), q*l1*l2 == q*r.
proof: Proof. intros; rewrite <- H; auto with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(BoolView)