proposition: Lemma per_add_edge_covariant : forall A (B1 B2 : binary A) x y, incl B1 B2 -> incl (per_add_edge B1 x y) (per_add_edge B2 x y).
proof: Proof. Proof using. unfold binary_incl. unfold per_add_edge. introv M. applys covariant_stclosure. applys* covariant_union. applys refl_rel_incl. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)