Misc: add in_set_cons lemma

ike-mulder-aws · ike-mulder-aws · commit cef2a9a9cb87 · 2026-05-18T12:09:31.000+01:00
Signed-off-by: Ike Mulder &lt;ikemul@amazon.com&gt;
diff --git a/Misc/SetAdditional.thy b/Misc/SetAdditional.thy
@@ -124,6 +124,10 @@ lemma LetE:
     shows \<open>Q\<close>
   using assms by simp
 
+lemma in_set_cons:
+  shows \<open>(x \<in> set (Cons y zs)) = (x = y \<or> x \<in> set zs)\<close>
+  by auto
+
 (*<*)
 end
 (*>*)
