theory Bug
  imports HOL.Argo HOL.Metis \<comment> \<open>A minimalistic import for faster propagation of changes in Argo\<close>
begin

lemma
  "\<not> subseteq
     (Field (image (apsnd Container) (rel (upd h_ent (Object ob) (single (pair c n))))))
     s'_entities \<longrightarrow>
   member 
     (w
       (Field (image (apsnd Container)
       (rel (upd h_ent (Object ob) (single (pair c n))))))
       s'_entities)
     (Field (image (apsnd Container) (rel (upd h_ent (Object ob) (single (pair c n)))))) \<and>
   \<not> member
       (w 
         (Field (image (apsnd Container)
         (rel (upd h_ent (Object ob) (single (pair c n))))))
         s'_entities)
       s'_entities \<Longrightarrow>
   s'_entities =
     insert (Object ob) (union (image Object objects) (image Container containers)) \<Longrightarrow>
   subseteq
     (Field (image (apsnd Container) (rel (upd h_ent (Object ob) (single (pair c n))))))
     (insert (Object ob) (union (image Object objects) (image Container containers)))"
  apply argo
  oops

\<comment> \<open>In case only \<^theory>\<open>HOL.Argo\<close> is imported
\<^theory_text>\<open>
typedecl 'a set
consts member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" ("_ \<in> _" [51, 51] 50)
consts image :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "`" 90)
\<close>
\<close>

lemma
 "w\<^sub>i = \<w>\<^sub>i (Object ob) Container containers \<Longrightarrow>
  w\<^sub>i\<^sub>0 = \<w>\<^sub>i (Object ob) Object objects \<Longrightarrow>
  Object ob \<in> Object ` objects \<longrightarrow>
    Object ob = Object (\<w>\<^sub>i (Object ob) Object objects) \<and>
    \<w>\<^sub>i (Object ob) Object objects \<in> objects \<Longrightarrow>
  Object ob \<in> Container ` containers \<longrightarrow>
    Object ob = Container (\<w>\<^sub>i (Object ob) Container containers) \<and>
    \<w>\<^sub>i (Object ob) Container containers \<in> containers \<Longrightarrow>
  \<t>\<^sub>e (Object ob) = zero \<Longrightarrow>
  \<t>\<^sub>e (Container w\<^sub>i) = one \<Longrightarrow>
  zero \<noteq> one \<Longrightarrow>
  object (Object w\<^sub>i\<^sub>0) = w\<^sub>i\<^sub>0 \<Longrightarrow>
  object (Object ob) = ob \<Longrightarrow>
  \<not>(ob \<in> objects) \<Longrightarrow>
  \<not>(Object ob \<in> Object ` objects) \<and> \<not>(Object ob \<in> Container ` containers)"
  apply argo apply metis
  oops
end