proposition: Lemma add_continuation A B (r: X A B) (p: forall Q, X Q A -> X Q B) (P: Prop): ((forall Q (q: X Q A), p _ q == q*r) -> P) -> (forall Q (q: X Q A), p _ q == q*r) -> P.
proof: Proof. tauto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(BoolView)