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