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. 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.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.