139  (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>

   139  (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>

   140  (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))

   140  (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))

   141 )"

   141 )"

   142 apply (lifting tolift)

   142 apply (lifting tolift)

   143 apply (regularize)

   143 apply (regularize)

   144 prefer 2

   145 prefer 2

   145 apply cleaning

   146 apply cleaning

   146 apply simp

   147 apply simp

   147 sorry

   148 sorry

   148 

   149