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