proposition: Lemma cgraph_mor_eq_aux {G H : precgraph} (p q : cgraph_mor G H) (e₀ : onnode p = onnode q) (e₁ : onarc p = onarc q) (h : has_nodeset H) : p = q.
proof: Proof. induction p as (p₀,(p₁,(psource,ptarget))). induction q as (q₀,(q₁,(qsource,qtarget))). cbn in *. induction e₀. apply pair_path_in2. induction e₁. apply pair_path_in2. apply pathsdirprod. - apply funextsec. intro f. apply h. - apply funextsec. intro f. apply h. Qed.
imports: UniMath.MoreFoundations.Propositions