proposition: Lemma pair_cocone_commutes {J : category} {d : diagram pair_graph J} {j : J} (cc : cocone d j) (e : edge pair_src pair_dst) : dmor d e · coconeIn cc pair_dst = coconeIn cc pair_src.
proof: Proof. exact(coconeInCommutes cc pair_src pair_dst e). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSets