proposition: Lemma isaprop_is_cgraph_mor {G H : precgraph} (p₀ : node G → node H) (p₁ : arc G → arc H) (h : has_nodeset H) : isaprop (is_cgraph_mor p₀ p₁).
proof: Proof. apply isapropdirprod; apply impred_isaprop; intro f; apply h. Qed.
imports: UniMath.MoreFoundations.Propositions