diff --git a/examples/generic_finite_graphs/genericGraphScript.sml b/examples/generic_finite_graphs/genericGraphScript.sml
index 2ed18517fc..08b0eb5537 100644
--- a/examples/generic_finite_graphs/genericGraphScript.sml
+++ b/examples/generic_finite_graphs/genericGraphScript.sml
@@ -396,6 +396,13 @@ Proof
   simp[emptyG0_def]
 QED
 
+Theorem nlabelfun_empty[simp]:
+  nlabelfun emptyG = (λn. ARB)
+Proof
+  simp[nlabelfun_def, emptyG_def, #repabs_pseudo_id tydefrec] >>
+  simp[emptyG0_def, FUN_EQ_THM]
+QED
+
 Definition adjacent_def:
   adjacent G n1 n2 ⇔ ∃l. (n1, n2, l) ∈ edges G
 End
@@ -682,6 +689,12 @@ Proof
   simp[oneEdge_max_def, itself2set_def]
 QED
 
+Theorem oneEdge_max_fdirgraph[simp]:
+  ¬oneEdge_max (g : (α,β,γ)fdirgraph)
+Proof
+  simp[oneEdge_max_def, itself2set_def]
+QED
+
 Theorem selfloops_ok_graph[simp]:
   selfloops_ok (g : ('a,'d,'ec,'el,'nf,'nl,unit) graph)
 Proof