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