As a follow up to Double Pushouts on Graphs I was trying to understand how things work when we add labels. This caused me some confusion, because I was wondering "which label does the edge get, when