proposition: Lemma cgraph_mor_eq {G H : cgraph} (p q : cgraph_mor G H) (e₀ : ∏ x : node G, onnode p x = onnode q x) (e₁ : ∏ f : arc G, onarc p f = onarc q f) : p = q.
proof: Proof. apply cgraph_mor_eq_aux. - apply funextfun. exact e₀. - apply funextfun. exact e₁. - apply isaset_node. Qed.
imports: UniMath.MoreFoundations.Propositions