Quelle  GFP.thy

(*  Title:       GFP
    Authors:     Jasmin Blanchette, Andrei Popescu, Dmitriy Traytel
    Maintainer:  Dmitriy Traytel <traytel at inf.ethz.ch>
*)

section ‹Greatest Fixpoint (a.k.a. Codatatype)›

(*<*)
theory GFP
  imports "HOL-Library.BNF_Axiomatization"
begin
(*>*)

unbundle cardinal_syntax

text ‹
 begin{tabular}{rcl}
 'b1 &=& ('a, 'b1, 'b2) F1\\
 'b2 &=& ('a, 'b1, 'b2) F2
 end{tabular}

  build a witness scenario, let us assume

 begin{tabular}{rcl}
 ('a, 'b1, 'b2) F1 &=& 'a * 'b1 + 'a * 'b2\\
 ('a, 'b1, 'b2) F2 &=& unit + 'b1 * 'b2
 end{tabular}
 ›

ML ‹open Ctr_Sugar_Util›
declare [[bnf_internals]]
bnf_axiomatization (F1set1: 'a, F1set2: 'b1, F1set3: 'b2)  F1
  [wits: "'a ==> 'b1 ==> ('a, 'b1, 'b2) F1" "'a ==> 'b2 ==> ('a, 'b1, 'b2) F1"]
  for map: F1map rel: F1rel

bnf_axiomatization (F2set1: 'a, F2set2: 'b1, F2set3: 'b2)  F2
  [wits: "('a, 'b1, 'b2) F2"]
  for map: F2map rel: F2rel

lemma F1rel_cong: "[R1 = S1; R2 = S2; R3 = S3] ==> F1rel R1 R2 R3 = F1rel S1 S2 S3"
  by hypsubst rule

lemma F2rel_cong: "[R1 = S1; R2 = S2; R3 = S3] ==> F2rel R1 R2 R3 = F2rel S1 S2 S3"
  by hypsubst rule

abbreviation F1in :: "'a1 set ==> 'a2 set ==> 'a3 set ==> (('a1, 'a2, 'a3) F1) set" where
  "F1in A1 A2 A3 ≡ {x. F1set1 x ⊆ A1 ∧ F1set2 x ⊆ A2 ∧ F1set3 x ⊆ A3}"
abbreviation F2in :: "'a1 set ==> 'a2 set ==> 'a3 set ==> (('a1, 'a2, 'a3) F2) set" where
  "F2in A1 A2 A3 ≡ {x. F2set1 x ⊆ A1 ∧ F2set2 x ⊆ A2 ∧ F2set3 x ⊆ A3}"

lemma F1map_comp_id: "F1map g1 g2 g3 (F1map id f2 f3 x) = F1map g1 (g2 o f2) (g3 o f3) x"
  apply (rule trans)
   apply (rule F1.map_comp)
  unfolding o_id
  apply (rule refl)
  done

lemmas F1in_mono23 = F1.in_mono[OF subset_refl]
lemmas F1in_mono23' = subsetD[OF F1in_mono23]

lemma F1map_congL: "[∀a ∈ F1set2 x. f a = a; ∀a ∈ F1set3 x. g a = a] ==>
  F1map id f g x = x"
  apply (rule trans)
   apply (rule F1.map_cong0)
     apply (rule refl)
    apply (rule trans)
     apply (erule bspec)
     apply assumption
    apply (rule sym)
    apply (rule id_apply)
   apply (rule trans)
    apply (erule bspec)
    apply assumption
   apply (rule sym)
   apply (rule id_apply)
  apply (rule F1.map_id)
  done

lemma F2map_comp_id: "F2map g1 g2 g3 (F2map id f2 f3 x) = F2map g1 (g2 o f2) (g3 o f3) x"
  apply (rule trans)
   apply (rule F2.map_comp)
  unfolding o_id
  apply (rule refl)
  done

lemmas F2in_mono23 = F2.in_mono[OF subset_refl]
lemmas F2in_mono23' = subsetD[OF F2in_mono23]

lemma F2map_congL: "[∀a ∈ F2set2 x. f a = a; ∀a ∈ F2set3 x. g a = a] ==>
  F2map id f g x = x"
  apply (rule trans)
   apply (rule F2.map_cong0)
     apply (rule refl)
    apply (rule trans)
     apply (erule bspec)
     apply assumption
    apply (rule sym)
    apply (rule id_apply)
   apply (rule trans)
    apply (erule bspec)
    apply assumption
   apply (rule sym)
   apply (rule id_apply)
  apply (rule F2.map_id)
  done

subsection ‹Coalgebra›

definition coalg where
  "coalg B1 B2 s1 s2 =
     ((∀a ∈ B1. s1 a ∈ F1in (UNIV :: 'a set) B1 B2) ∧ (∀a ∈ B2. s2 a ∈ F2in (UNIV :: 'a set) B1 B2))"

lemmas coalg_F1in = bspec[OF conjunct1[OF iffD1[OF coalg_def]]]
lemmas coalg_F2in = bspec[OF conjunct2[OF iffD1[OF coalg_def]]]

lemma coalg_F1set2:
  "[coalg B1 B2 s1 s2; a ∈ B1] ==> F1set2 (s1 a) ⊆ B1"
  apply (tactic ‹dtac @{context} @{thm iffD1[OF coalg_def]} 1›)
  apply (erule conjE)
  apply (drule bspec[rotated])
   apply assumption
  apply (erule CollectE conjE)+
  apply assumption
  done

lemma coalg_F1set3:
  "[coalg B1 B2 s1 s2; a ∈ B1] ==> F1set3 (s1 a) ⊆ B2"
  apply (tactic ‹dtac @{context} @{thm iffD1[OF coalg_def]} 1›)
  apply (erule conjE)
  apply (drule bspec[rotated])
   apply assumption
  apply (erule CollectE conjE)+
  apply assumption
  done

lemma coalg_F2set2:
  "[coalg B1 B2 s1 s2; a ∈ B2] ==> F2set2 (s2 a) ⊆ B1"
  apply (tactic ‹dtac @{context} @{thm iffD1[OF coalg_def]} 1›)
  apply (erule conjE)
  apply (drule bspec[rotated])
   apply assumption
  apply (erule CollectE conjE)+
  apply assumption
  done

lemma coalg_F2set3:
  "[coalg B1 B2 s1 s2; a ∈ B2] ==> F2set3 (s2 a) ⊆ B2"
  apply (tactic ‹dtac @{context} @{thm iffD1[OF coalg_def]} 1›)
  apply (erule conjE)
  apply (drule bspec[rotated])
   apply assumption
  apply (erule CollectE conjE)+
  apply assumption
  done


subsection‹Type-coalgebra›

abbreviation "tcoalg s1 s2 ≡ coalg UNIV UNIV s1 s2"

lemma tcoalg: "tcoalg s1 s2"
  apply (tactic ‹rtac @{context} (@{thm coalg_def} RS iffD2) 1›)
  apply (rule conjI)
   apply (rule ballI)
   apply (rule CollectI)
   apply (rule conjI)
    apply (rule subset_UNIV)
   apply (rule conjI)
    apply (rule subset_UNIV)
   apply (rule subset_UNIV)
  apply (rule ballI)
  apply (rule CollectI)
  apply (rule conjI)
   apply (rule subset_UNIV)
  apply (rule conjI)
   apply (rule subset_UNIV)
  apply (rule subset_UNIV)
  done


subsection ‹Morphism›

definition mor where
  "mor B1 B2 s1 s2 B1' B2' s1' s2' f g =
   (((∀a ∈ B1. f a ∈ B1') ∧ (∀a ∈ B2. g a ∈ B2')) ∧
   ((∀z ∈ B1. F1map (id :: 'a ==> 'a) f g (s1 z) = s1' (f z)) ∧
     (∀z ∈ B2. F2map (id :: 'a ==> 'a) f g (s2 z) = s2' (g z))))"

lemma mor_image1: "mor B1 B2 s1 s2 B1' B2' s1' s2' f g ==> f ` B1 ⊆ B1'"
  apply (tactic ‹dtac @{context} @{thm iffD1[OF mor_def]} 1›)
  apply (erule conjE)+
  apply (rule image_subsetI)
  apply (erule bspec)
  apply assumption
  done

lemma mor_image2: "mor B1 B2 s1 s2 B1' B2' s1' s2' f g ==> g ` B2 ⊆ B2'"
  apply (tactic ‹dtac @{context} @{thm iffD1[OF mor_def]} 1›)
  apply (erule conjE)+
  apply (rule image_subsetI)
  apply (erule bspec)
  apply assumption
  done

lemmas mor_image1' = subsetD[OF mor_image1 imageI]
lemmas mor_image2' = subsetD[OF mor_image2 imageI]

lemma morE1: "[mor B1 B2 s1 s2 B1' B2' s1' s2' f g; z ∈ B1]
   ==> F1map id f g (s1 z) = s1' (f z)"
  apply (tactic ‹dtac @{context} @{thm iffD1[OF mor_def]} 1›)
  apply (erule conjE)+
  apply (erule bspec)
  apply assumption
  done

lemma morE2: "[mor B1 B2 s1 s2 B1' B2' s1' s2' f g; z ∈ B2]
   ==> F2map id f g (s2 z) = s2' (g z)"
  apply (tactic ‹dtac @{context} @{thm iffD1[OF mor_def]} 1›)
  apply (erule conjE)+
  apply (erule bspec)
  apply assumption
  done

lemma mor_incl: "[B1 ⊆ B1'; B2 ⊆ B2'] ==> mor B1 B2 s1 s2 B1' B2' s1 s2 id id"
  apply (tactic ‹rtac @{context} (@{thm mor_def} RS iffD2) 1›)
  apply (rule conjI)
   apply (rule conjI)
    apply (rule ballI)
    apply (rule ssubst_mem[OF id_apply])
    apply (erule subsetD)
    apply assumption

   apply (rule ballI)
   apply (rule ssubst_mem[OF id_apply])
   apply (erule subsetD)
   apply assumption

  apply (rule conjI)
   apply (rule ballI)
   apply (rule trans[OF F1.map_id])
   apply (rule sym)
   apply (rule arg_cong[OF id_apply])
  apply (rule ballI)
  apply (rule trans[OF F2.map_id])
  apply (rule sym)
  apply (rule arg_cong[OF id_apply])
  done

lemmas mor_id = mor_incl[OF subset_refl subset_refl]

lemma mor_comp:
  "[mor B1 B2 s1 s2 B1' B2' s1' s2' f g;
    mor B1' B2' s1' s2' B1'' B2'' s1'' s2'' f' g'] ==>
   mor B1 B2 s1 s2 B1'' B2'' s1'' s2'' (f' o f) (g' o g)"
  apply (tactic ‹rtac @{context} (@{thm mor_def} RS iffD2) 1›)
  apply (rule conjI)

   apply (rule conjI)
    apply (rule ballI)
    apply (rule ssubst_mem[OF o_apply])
    apply (erule mor_image1')
    apply (erule mor_image1')
    apply assumption

   apply (rule ballI)
   apply (rule ssubst_mem[OF o_apply])
   apply (erule mor_image2')
   apply (erule mor_image2')
   apply assumption

  apply (rule conjI)
   apply (rule ballI)
   apply (tactic ‹stac @{context} @{thm o_apply} 1›)
   apply (rule trans)
    apply (rule sym[OF F1map_comp_id])
   apply (rule trans)
    apply (erule arg_cong[OF morE1])
    apply assumption
   apply (erule morE1)
   apply (erule mor_image1')
   apply assumption

  apply (rule ballI)
  apply (tactic ‹stac @{context} @{thm o_apply} 1›)
  apply (rule trans)
   apply (rule sym[OF F2map_comp_id])
  apply (rule trans)
   apply (erule arg_cong[OF morE2])
   apply assumption
  apply (erule morE2)
  apply (erule mor_image2')
  apply assumption
  done

lemma mor_cong: "[ f' = f; g' = g; mor B1 B2 s1 s2 B1' B2' s1' s2' f g] ==>
  mor B1 B2 s1 s2 B1' B2' s1' s2' f' g'"
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply assumption
  done

lemma mor_UNIV: "mor UNIV UNIV s1 s2 UNIV UNIV s1' s2' f1 f2 ⟷
  F1map id f1 f2 o s1 = s1' o f1 ∧ F2map id f1 f2 o s2 = s2' o f2"
  apply (rule iffI)
   apply (rule conjI)
    apply (rule ext)
    apply (rule trans)
     apply (rule trans)
      apply (rule o_apply)
     apply (erule morE1)
     apply (rule UNIV_I)
    apply (rule sym[OF o_apply])
   apply (rule ext)
   apply (rule trans)
    apply (rule trans)
     apply (rule o_apply)
    apply (erule morE2)
    apply (rule UNIV_I)
   apply (rule sym[OF o_apply])

  apply (tactic ‹rtac @{context} (@{thm mor_def} RS iffD2) 1›)
  apply (rule conjI)
   apply (rule conjI)
    apply (rule ballI)
    apply (rule UNIV_I)
   apply (rule ballI)
   apply (rule UNIV_I)
  apply (rule conjI)
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (rule ballI)
   apply (erule o_eq_dest)
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (rule ballI)
  apply (erule o_eq_dest)
  done

lemma mor_str:
  "mor UNIV UNIV s1 s2 UNIV UNIV (F1map id s1 s2) (F2map id s1 s2) s1 s2"
  apply (rule iffD2)
   apply (rule mor_UNIV)
  apply (rule conjI)
   apply (rule refl)
  apply (rule refl)
  done

lemma mor_case_sum:
  "mor UNIV UNIV s1 s2 UNIV UNIV (case_sum (F1map id Inl Inl o s1) s1') (case_sum (F2map id Inl Inl o s2) s2') Inl Inl"
  apply (tactic ‹rtac @{context} (@{thm mor_UNIV} RS iffD2) 1›)
  apply (rule conjI)
   apply (rule sym)
   apply (rule case_sum_o_inj(1))
  apply (rule sym)
  apply (rule case_sum_o_inj(1))
  done

subsection ‹Bisimulations›

definition bis where
  "bis B1 B2 s1 s2 B1' B2' s1' s2' R1 R2 =
   ((R1 ⊆ B1 × B1' ∧ R2 ⊆ B2 × B2') ∧
   ((∀b1 b1'. (b1, b1') ∈ R1 ⟶
     (∃z ∈ F1in UNIV R1 R2.
       F1map id fst fst z = s1 b1 ∧ F1map id snd snd z = s1' b1')) ∧
    (∀b2 b2'. (b2, b2') ∈ R2 ⟶
     (∃z ∈ F2in UNIV R1 R2.
       F2map id fst fst z = s2 b2 ∧ F2map id snd snd z = s2' b2'))))"

lemma bis_cong: "[bis B1 B2 s1 s2 B1' B2' s1' s2' R1 R2; R1' = R1; R2' = R2] ==>
  bis B1 B2 s1 s2 B1' B2' s1' s2' R1' R2'"
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply assumption
  done

lemma bis_Frel:
  "bis B1 B2 s1 s2 B1' B2' s1' s2' R1 R2 ⟷
  (R1 ⊆ B1 × B1' ∧ R2 ⊆ B2 × B2') ∧
  ((∀ b1 b1'. (b1, b1') ∈ R1 ⟶ F1rel (=) (in_rel R1) (in_rel R2) (s1 b1) (s1' b1')) ∧
   (∀ b2 b2'. (b2, b2') ∈ R2 ⟶ F2rel (=) (in_rel R1) (in_rel R2) (s2 b2) (s2' b2')))"
  apply (rule trans[OF bis_def])
  apply (rule iffI)
   apply (erule conjE)
   apply (erule conjI)

   apply (rule conjI)
    apply (rule allI)
    apply (rule allI)
    apply (rule impI)
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule allE)+
    apply (erule impE)
     apply assumption
    apply (erule bexE)
    apply (erule conjE CollectE)+
    apply (rule iffD2[OF F1.in_rel])
    apply (rule exI)
    apply (rule conjI[rotated])
     apply (rule conjI)
      apply (rule trans)
       apply (rule trans)
        apply (rule F1.map_comp)
       apply (rule F1.map_cong0)
         apply (rule fst_diag_id)
        apply (rule fun_cong[OF o_id])
       apply (rule fun_cong[OF o_id])
      apply assumption

     apply (rule trans)
      apply (rule trans)
       apply (rule F1.map_comp)
      apply (rule F1.map_cong0)
        apply (rule snd_diag_id)
       apply (rule fun_cong[OF o_id])
      apply (rule fun_cong[OF o_id])
     apply assumption

    apply (rule CollectI)
    apply (rule conjI)
     apply (rule ord_eq_le_trans)
      apply (rule F1.set_map(1))
     apply (rule subset_trans)
      apply (erule image_mono)
     apply (rule image_subsetI)
     apply (rule CollectI)
     apply (rule case_prodI)
     apply (rule refl)
    apply (rule conjI)
     apply (rule ord_eq_le_trans)
      apply (rule trans)
       apply (rule F1.set_map(2))
      apply (rule trans[OF fun_cong[OF image_id] id_apply])
     apply (erule Collect_case_prod_in_rel_leI)
    apply (rule ord_eq_le_trans)
     apply (rule trans)
      apply (rule F1.set_map(3))
     apply (rule trans[OF fun_cong[OF image_id] id_apply])
    apply (erule Collect_case_prod_in_rel_leI)

   apply (rule allI)
   apply (rule allI)
   apply (rule impI)
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule allE)+
   apply (erule impE)
    apply assumption
   apply (erule bexE)
   apply (erule conjE CollectE)+
   apply (rule iffD2[OF F2.in_rel])
   apply (rule exI)
   apply (rule conjI[rotated])
    apply (rule conjI)
     apply (rule trans)
      apply (rule trans)
       apply (rule F2.map_comp)
      apply (rule F2.map_cong0)
        apply (rule fst_diag_id)
       apply (rule fun_cong[OF o_id])
      apply (rule fun_cong[OF o_id])
     apply assumption

    apply (rule trans)
     apply (rule trans)
      apply (rule F2.map_comp)
     apply (rule F2.map_cong0)
       apply (rule snd_diag_id)
      apply (rule fun_cong[OF o_id])
     apply (rule fun_cong[OF o_id])
    apply assumption

   apply (rule CollectI)
   apply (rule conjI)
    apply (rule ord_eq_le_trans)
     apply (rule F2.set_map(1))
    apply (rule subset_trans)
     apply (erule image_mono)
    apply (rule image_subsetI)
    apply (rule CollectI)
    apply (rule case_prodI)
    apply (rule refl)
   apply (rule conjI)
    apply (rule ord_eq_le_trans)
     apply (rule trans)
      apply (rule F2.set_map(2))
     apply (rule trans[OF fun_cong[OF image_id] id_apply])
    apply (erule Collect_case_prod_in_rel_leI)
   apply (rule ord_eq_le_trans)
    apply (rule trans)
     apply (rule F2.set_map(3))
    apply (rule trans[OF fun_cong[OF image_id] id_apply])
   apply (erule Collect_case_prod_in_rel_leI)

  apply (erule conjE)
  apply (erule conjI)

  apply (rule conjI)
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (rule allI)
   apply (rule allI)
   apply (rule impI)
   apply (erule allE)
   apply (erule allE)
   apply (erule impE)
    apply assumption
   apply (drule iffD1[OF F1.in_rel])
   apply (erule exE conjE CollectE Collect_case_prod_in_rel_leE)+

(*F1rel_bis_su*)
   apply (rule bexI)
    apply (rule conjI)
     apply (rule trans)
      apply (rule F1.map_comp)
     apply (tactic ‹stac @{context} @{thm id_o} 1›)
     apply (tactic ‹stac @{context} @{thm o_id} 1›)
     apply (tactic ‹stac @{context} @{thm o_id} 1›)
     apply assumption

    apply (rule trans)
     apply (rule F1.map_comp)
    apply (tactic ‹stac @{context} @{thm id_o} 1›)
    apply (tactic ‹stac @{context} @{thm o_id} 1›)
    apply (tactic ‹stac @{context} @{thm o_id} 1›)
    apply (rule trans)
     apply (rule F1.map_cong0)
       apply (rule Collect_case_prodD)
       apply (erule subsetD)
       apply assumption
      apply (rule refl)
     apply (rule refl)
    apply assumption

   apply (rule CollectI)
   apply (rule conjI)
    apply (rule subset_UNIV)

   apply (rule conjI)
    apply (rule ord_eq_le_trans)
     apply (rule trans)
      apply (rule F1.set_map(2))
     apply (rule trans[OF fun_cong[OF image_id] id_apply])
    apply assumption

   apply (rule ord_eq_le_trans)
    apply (rule trans)
     apply (rule F1.set_map(3))
    apply (rule trans[OF fun_cong[OF image_id] id_apply])
   apply assumption

  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (rule allI)
  apply (rule allI)
  apply (rule impI)
  apply (erule allE)
  apply (erule allE)
  apply (erule impE)
   apply assumption
  apply (drule iffD1[OF F2.in_rel])
  apply (erule exE conjE CollectE Collect_case_prod_in_rel_leE)+

(*F2rel_bis_su*)
  apply (rule bexI)
   apply (rule conjI)
    apply (rule trans)
     apply (rule F2.map_comp)
    apply (tactic ‹stac @{context} @{thm id_o} 1›)
    apply (tactic ‹stac @{context} @{thm o_id} 1›)
    apply (tactic ‹stac @{context} @{thm o_id} 1›)
    apply assumption

   apply (rule trans)
    apply (rule F2.map_comp)
   apply (tactic ‹stac @{context} @{thm id_o} 1›)
   apply (tactic ‹stac @{context} @{thm o_id} 1›)
   apply (tactic ‹stac @{context} @{thm o_id} 1›)
   apply (rule trans)
    apply (rule F2.map_cong0)
      apply (rule Collect_case_prodD)
      apply (erule subsetD)
      apply assumption
     apply (rule refl)
    apply (rule refl)
   apply assumption

  apply (rule CollectI)
  apply (rule conjI)
   apply (rule subset_UNIV)

  apply (rule conjI)
   apply (rule ord_eq_le_trans)
    apply (rule trans)
     apply (rule F2.set_map(2))
    apply (rule trans[OF fun_cong[OF image_id] id_apply])
   apply assumption

  apply (rule ord_eq_le_trans)
   apply (rule trans)
    apply (rule F2.set_map(3))
   apply (rule trans[OF fun_cong[OF image_id] id_apply])
  apply assumption
  done

lemma bis_converse:
  "bis B1 B2 s1 s2 B1' B2' s1' s2' R1 R2 ==>
   bis B1' B2' s1' s2' B1 B2 s1 s2 (R1^-1) (R2^-1)"
  apply (tactic ‹rtac @{context} (@{thm bis_Frel} RS iffD2) 1›)
  apply (tactic ‹dtac @{context} (@{thm bis_Frel} RS iffD1) 1›)
  apply (erule conjE)+
  apply (rule conjI)

   apply (rule conjI)
    apply (rule iffD1[OF converse_subset_swap])
    apply (erule subset_trans)
    apply (rule equalityD2)
    apply (rule converse_Times)

   apply (rule iffD1[OF converse_subset_swap])
   apply (erule subset_trans)
   apply (rule equalityD2)
   apply (rule converse_Times)

  apply (rule conjI)
   apply (rule allI)
   apply (rule allI)
   apply (rule impI)
   apply (rule predicate2D[OF eq_refl[OF F1rel_cong]])
      apply (rule conversep_eq)
     apply (rule conversep_in_rel)
    apply (rule conversep_in_rel)
   apply (rule predicate2D[OF eq_refl[OF sym[OF F1.rel_conversep]]])
   apply (erule allE)+
   apply (rule conversepI)
   apply (erule mp)
   apply (erule converseD)

  apply (rule allI)
  apply (rule allI)
  apply (rule impI)
  apply (rule predicate2D[OF eq_refl[OF F2rel_cong]])
     apply (rule conversep_eq)
    apply (rule conversep_in_rel)
   apply (rule conversep_in_rel)
  apply (rule predicate2D[OF eq_refl[OF sym[OF F2.rel_conversep]]])
  apply (erule allE)+
  apply (rule conversepI)
  apply (erule mp)
  apply (erule converseD)
  done

lemma bis_Comp:
  "[bis B1 B2 s1 s2 B1' B2' s1' s2' P1 P2;
    bis B1' B2' s1' s2' B1'' B2'' s1'' s2'' Q1 Q2] ==>
    bis B1 B2 s1 s2 B1'' B2'' s1'' s2'' (P1 O Q1) (P2 O Q2)"
  apply (tactic ‹rtac @{context} (@{thm bis_Frel[THEN iffD2]}) 1›)
  apply (tactic ‹dtac @{context} (@{thm bis_Frel[THEN iffD1]}) 1›)+
  apply (erule conjE)+
  apply (rule conjI)
   apply (rule conjI)
    apply (erule relcomp_subset_Sigma)
    apply assumption
   apply (erule relcomp_subset_Sigma)
   apply assumption

  apply (rule conjI)
   apply (rule allI)+
   apply (rule impI)
   apply (rule predicate2D[OF eq_refl[OF F1rel_cong]])
      apply (rule eq_OO)
     apply (rule relcompp_in_rel)
    apply (rule relcompp_in_rel)
   apply (rule predicate2D[OF eq_refl[OF sym[OF F1.rel_compp]]])
   apply (erule relcompE)
   apply (tactic ‹dtac @{context} (@{thm prod.inject[THEN iffD1]}) 1›)
   apply (erule conjE)
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (erule allE)+
   apply (rule relcomppI)
    apply (erule mp)
    apply assumption
   apply (erule mp)
   apply assumption

  apply (rule allI)+
  apply (rule impI)
  apply (rule predicate2D[OF eq_refl[OF F2rel_cong]])
     apply (rule eq_OO)
    apply (rule relcompp_in_rel)
   apply (rule relcompp_in_rel)
  apply (rule predicate2D[OF eq_refl[OF sym[OF F2.rel_compp]]])
  apply (erule relcompE)
  apply (tactic ‹dtac @{context} (@{thm prod.inject[THEN iffD1]}) 1›)
  apply (erule conjE)
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (erule allE)+
  apply (rule relcomppI)
   apply (erule mp)
   apply assumption
  apply (erule mp)
  apply assumption
  done

lemma bis_Gr: "[coalg B1 B2 s1 s2; mor B1 B2 s1 s2 B1' B2' s1' s2' f1 f2] ==>
   bis B1 B2 s1 s2 B1' B2' s1' s2' (BNF_Def.Gr B1 f1) (BNF_Def.Gr B2 f2)"
  unfolding bis_Frel eq_alt in_rel_Gr F1.rel_Grp F2.rel_Grp
  apply (rule conjI)
   apply (rule conjI)
    apply (rule iffD2[OF Gr_incl])
    apply (erule mor_image1)
   apply (rule iffD2[OF Gr_incl])
   apply (erule mor_image2)

  apply (rule conjI)
   apply (rule allI)
   apply (rule allI)
   apply (rule impI)
   apply (rule GrpI)
    apply (erule trans[OF morE1])
     apply (erule GrD1)
    apply (erule arg_cong[OF GrD2])
   apply (erule coalg_F1in)
   apply (erule GrD1)

  apply (rule allI)
  apply (rule allI)
  apply (rule impI)
  apply (rule GrpI)
   apply (erule trans[OF morE2])
    apply (erule GrD1)
   apply (erule arg_cong[OF GrD2])
  apply (erule coalg_F2in)
  apply (erule GrD1)
  done

lemmas bis_image2 = bis_cong[OF bis_Comp[OF bis_converse[OF bis_Gr] bis_Gr] image2_Gr image2_Gr]
lemmas bis_diag = bis_cong[OF bis_Gr[OF _ mor_id] Id_on_Gr Id_on_Gr]

lemma bis_Union: "∀i ∈ I. bis B1 B2 s1 s2 B1 B2 s1 s2 (R1i i) (R2i i) ==>
  bis B1 B2 s1 s2 B1 B2 s1 s2 (∪i∈ I. R1i i) (∪i∈ I. R2i i)"
  unfolding bis_def
  apply (rule conjI)
   apply (rule conjI)
    apply (rule UN_least)
    apply (drule bspec)
     apply assumption
    apply (drule conjunct1)
    apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (rule UN_least)
   apply (drule bspec)
    apply assumption
   apply (drule conjunct1)
   apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)

  apply (rule conjI)
   apply (rule allI)+
   apply (rule impI)
   apply (erule UN_E)
   apply (drule bspec)
    apply assumption
   apply (drule conjunct2)
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (erule allE)+
   apply (drule mp)
    apply assumption
   apply (erule bexE)
   apply (rule bexI)
    apply assumption
   apply (rule F1in_mono23')
     apply (erule SUP_upper2[OF _ subset_refl])
    apply (erule SUP_upper2[OF _ subset_refl])
   apply assumption

  apply (rule allI)+
  apply (rule impI)
  apply (erule UN_E)
  apply (drule bspec)
   apply assumption
  apply (drule conjunct2)
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (erule allE)+
  apply (drule mp)
   apply assumption
  apply (erule bexE)
  apply (rule bexI)
   apply assumption
  apply (rule F2in_mono23')
    apply (erule SUP_upper2[OF _ subset_refl])
   apply (erule SUP_upper2[OF _ subset_refl])
  apply assumption
  done

(* self-bisimulation: *)
abbreviation "sbis B1 B2 s1 s2 R1 R2 ≡ bis B1 B2 s1 s2 B1 B2 s1 s2 R1 R2"

(* The greatest self-bisimulation *)
definition lsbis1 where "lsbis1 B1 B2 s1 s2 =
  (∪R ∈ {(R1, R2) | R1 R2 . sbis B1 B2 s1 s2 R1 R2}. fst R)"

definition lsbis2 where "lsbis2 B1 B2 s1 s2 =
  (∪R ∈ {(R1, R2) | R1 R2 . sbis B1 B2 s1 s2 R1 R2}. snd R)"

lemma sbis_lsbis:
  "sbis B1 B2 s1 s2 (lsbis1 B1 B2 s1 s2) (lsbis2 B1 B2 s1 s2)"
  apply (tactic ‹rtac @{context} (Thm.permute_prems 0 1 @{thm bis_cong}) 1›)
    apply (rule lsbis1_def)
   apply (rule lsbis2_def)
  apply (rule bis_Union)
  apply (rule ballI)
  apply (erule CollectE exE conjE)+
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (erule bis_cong)
   apply (rule fst_conv)
  apply (rule snd_conv)
  done

lemmas lsbis1_incl = conjunct1[OF conjunct1[OF iffD1[OF bis_def]], OF sbis_lsbis]
lemmas lsbis2_incl = conjunct2[OF conjunct1[OF iffD1[OF bis_def]], OF sbis_lsbis]
lemmas lsbisE1 =
  mp[OF spec[OF spec[OF conjunct1[OF conjunct2[OF iffD1[OF bis_def]], OF sbis_lsbis]]]]
lemmas lsbisE2 =
  mp[OF spec[OF spec[OF conjunct2[OF conjunct2[OF iffD1[OF bis_def]], OF sbis_lsbis]]]]

lemma incl_lsbis1: "sbis B1 B2 s1 s2 R1 R2 ==> R1 ⊆ lsbis1 B1 B2 s1 s2"
  apply (rule xt1(3))
   apply (rule lsbis1_def)
  apply (rule SUP_upper2)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply assumption
  apply (rule equalityD2)
  apply (rule fst_conv)
  done

lemma incl_lsbis2: "sbis B1 B2 s1 s2 R1 R2 ==> R2 ⊆ lsbis2 B1 B2 s1 s2"
  apply (rule xt1(3))
   apply (rule lsbis2_def)
  apply (rule SUP_upper2)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply assumption
  apply (rule equalityD2)
  apply (rule snd_conv)
  done

lemma equiv_lsbis1: "coalg B1 B2 s1 s2 ==> equiv B1 (lsbis1 B1 B2 s1 s2)"
  apply (rule equivI)
     apply (rule lsbis1_incl)

    apply (rule refl_onI)
    apply (rule subsetD)
     apply (rule incl_lsbis1)
     apply (rule bis_diag)
     apply assumption
    apply (erule Id_onI)

   apply (rule symI)
   apply (rule subsetD)
    apply (rule incl_lsbis1)
    apply (rule bis_converse)
    apply (rule sbis_lsbis)
   apply (erule converseI)

  apply (rule iffD2[OF trans_def])
  apply (rule allI)+
  apply (rule impI)+
  apply (rule subsetD)
   apply (rule incl_lsbis1)
   apply (rule bis_Comp)
    apply (rule sbis_lsbis)
   apply (rule sbis_lsbis)
  apply (erule relcompI)
  apply assumption
  done

lemma equiv_lsbis2: "coalg B1 B2 s1 s2 ==> equiv B2 (lsbis2 B1 B2 s1 s2)"
  unfolding equiv_def refl_on_def sym_def trans_def
  apply (rule conjI)
    apply (rule lsbis2_incl)

   apply (rule conjI)
   apply (rule ballI)
   apply (rule subsetD)
    apply (rule incl_lsbis2)
    apply (rule bis_diag)
    apply assumption
   apply (erule Id_onI)

  apply (rule conjI)

   apply (rule allI)+
   apply (rule impI)
   apply (rule subsetD)
    apply (rule incl_lsbis2)
    apply (rule bis_converse)
    apply (rule sbis_lsbis)
   apply (erule converseI)

  apply (rule allI)+
  apply (rule impI)+
  apply (rule subsetD)
   apply (rule incl_lsbis2)
   apply (rule bis_Comp)
    apply (rule sbis_lsbis)
   apply (rule sbis_lsbis)
  apply (erule relcompI)
  apply assumption
  done


subsection ‹The Tree Coalgebra›

typedef bd_type_F = "UNIV :: (bd_type_F1 + bd_type_F2) suc set"
  apply (rule exI) apply (rule UNIV_I)
  done

type_synonym 'a carrier = "((bd_type_F + bd_type_F) list set ×
  ((bd_type_F + bd_type_F) list ==> (('a, bd_type_F, bd_type_F) F1 + ('a, bd_type_F, bd_type_F) F2)))"

abbreviation "bd_F ≡ dir_image (card_suc (bd_F1 +c bd_F2)) Abs_bd_type_F"

lemmas sum_card_order = card_order_csum[OF F1.bd_card_order F2.bd_card_order]
lemmas sum_Cinfinite = Cinfinite_csum1[OF F1.bd_Cinfinite]
lemmas bd_F = dir_image[OF Abs_bd_type_F_inject[OF UNIV_I UNIV_I] Card_order_card_suc[OF sum_card_order]]
lemmas bd_F_Cinfinite = Cinfinite_cong[OF bd_F Cinfinite_card_suc[OF sum_Cinfinite sum_card_order]]
lemmas bd_F_Card_order = Card_order_ordIso[OF Card_order_card_suc[OF sum_card_order] ordIso_symmetric[OF bd_F]]
lemma bd_F_card_order: "card_order bd_F"
  apply (rule card_order_dir_image)
   apply (rule bijI')
    apply (rule Abs_bd_type_F_inject[OF UNIV_I UNIV_I])
   apply (rule Abs_bd_type_F_cases)
   apply (erule exI)
  apply (rule card_order_card_suc)
  apply (rule sum_card_order)
  done
lemmas bd_F_regularCard = regularCard_ordIso[OF bd_F Cinfinite_card_suc[OF sum_Cinfinite sum_card_order]
  regularCard_card_suc[OF sum_card_order sum_Cinfinite]
]

lemmas F1set1_bd' = ordLess_transitive[OF F1.set_bd(1) ordLess_ordIso_trans[OF
  ordLeq_ordLess_trans[OF ordLeq_csum1[OF F1.bd_Card_order] card_suc_greater[OF sum_card_order]]
bd_F]]
lemmas F1set2_bd' = ordLess_transitive[OF F1.set_bd(2) ordLess_ordIso_trans[OF
  ordLeq_ordLess_trans[OF ordLeq_csum1[OF F1.bd_Card_order] card_suc_greater[OF sum_card_order]]
bd_F]]
lemmas F1set3_bd' = ordLess_transitive[OF F1.set_bd(3) ordLess_ordIso_trans[OF
  ordLeq_ordLess_trans[OF ordLeq_csum1[OF F1.bd_Card_order] card_suc_greater[OF sum_card_order]]
bd_F]]

lemmas F2set1_bd' = ordLess_transitive[OF F2.set_bd(1) ordLess_ordIso_trans[OF
  ordLeq_ordLess_trans[OF ordLeq_csum2[OF F2.bd_Card_order] card_suc_greater[OF sum_card_order]]
bd_F]]
lemmas F2set2_bd' = ordLess_transitive[OF F2.set_bd(2) ordLess_ordIso_trans[OF
  ordLeq_ordLess_trans[OF ordLeq_csum2[OF F2.bd_Card_order] card_suc_greater[OF sum_card_order]]
bd_F]]
lemmas F2set3_bd' = ordLess_transitive[OF F2.set_bd(3) ordLess_ordIso_trans[OF
  ordLeq_ordLess_trans[OF ordLeq_csum2[OF F2.bd_Card_order] card_suc_greater[OF sum_card_order]]
bd_F]]

abbreviation "Succ1 Kl kl ≡ {k1. Inl k1 ∈ BNF_Greatest_Fixpoint.Succ Kl kl}"
abbreviation "Succ2 Kl kl ≡ {k2. Inr k2 ∈ BNF_Greatest_Fixpoint.Succ Kl kl}"

definition isNode1 where
  "isNode1 Kl lab kl = (∃x1. lab kl = Inl x1 ∧ F1set2 x1 = Succ1 Kl kl ∧ F1set3 x1 = Succ2 Kl kl)"

definition isNode2 where
  "isNode2 Kl lab kl = (∃x2. lab kl = Inr x2 ∧ F2set2 x2 = Succ1 Kl kl ∧ F2set3 x2 = Succ2 Kl kl)"

abbreviation isTree where
  "isTree Kl lab ≡ ([] ∈ Kl ∧
 (∀kl ∈ Kl. (∀k1 ∈ Succ1 Kl kl. isNode1 Kl lab (kl @ [Inl k1])) ∧
            (∀k2 ∈ Succ2 Kl kl. isNode2 Kl lab (kl @ [Inr k2]))))"

definition carT1 where
  "carT1 = {(Kl :: (bd_type_F + bd_type_F) list set, lab) | Kl lab. isTree Kl lab ∧ isNode1 Kl lab []}"

definition carT2 where
  "carT2 = {(Kl :: (bd_type_F + bd_type_F) list set, lab) | Kl lab. isTree Kl lab ∧ isNode2 Kl lab []}"

definition strT1 where
  "strT1 = (case_prod (%Kl lab. case_sum (F1map id
       (λk1. (BNF_Greatest_Fixpoint.Shift Kl (Inl k1), BNF_Greatest_Fixpoint.shift lab (Inl k1)))
       (λk2. (BNF_Greatest_Fixpoint.Shift Kl (Inr k2), BNF_Greatest_Fixpoint.shift lab (Inr k2)))) undefined (lab [])))"

definition strT2 where
  "strT2 = (case_prod (%Kl lab. case_sum undefined (F2map id
       (λk1. (BNF_Greatest_Fixpoint.Shift Kl (Inl k1), BNF_Greatest_Fixpoint.shift lab (Inl k1)))
       (λk2. (BNF_Greatest_Fixpoint.Shift Kl (Inr k2), BNF_Greatest_Fixpoint.shift lab (Inr k2)))) (lab [])))"

lemma coalg_T: "coalg carT1 carT2 strT1 strT2"
  unfolding coalg_def carT1_def carT2_def isNode1_def isNode2_def
  apply (rule conjI)
   apply (rule ballI)
   apply (erule CollectE exE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule ssubst_mem[OF trans[OF trans[OF fun_cong[OF strT1_def] prod.case]]])
    apply (erule trans[OF arg_cong])
    apply (rule sum.case(1))
   apply (rule CollectI)
   apply (rule conjI)
    apply (rule subset_UNIV)
   apply (rule conjI)
    apply (rule ord_eq_le_trans[OF F1.set_map(2)])
    apply (rule image_subsetI)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (rule conjI)
     apply (rule conjI)
      apply (erule empty_Shift)
      apply (drule rev_subsetD)
       apply (erule equalityD1)
      apply (erule CollectD)
     apply (rule ballI)
     apply (rule conjI)
      apply (rule ballI)
      apply (erule CollectE)
      apply (drule ShiftD)
      apply (drule bspec)
       apply (erule thin_rl)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (drule bspec)
       apply (rule CollectI)
       apply (erule subsetD[OF equalityD1[OF Succ_Shift]])
      apply (erule exE conjE)+
      apply (rule exI)
      apply (rule conjI)
       apply (rule trans[OF fun_cong[OF shift_def]])
       apply (rule trans[OF arg_cong[OF sym[OF append_Cons]]])
       apply assumption
      apply (rule conjI)
       apply (erule trans)
       apply (rule Collect_cong)
       apply (rule eqset_imp_iff)
       apply (rule sym)
       apply (rule trans)
        apply (rule Succ_Shift)
       apply (rule arg_cong[OF sym[OF append_Cons]])
      apply (erule trans)
      apply (rule Collect_cong)
      apply (rule eqset_imp_iff)
      apply (rule sym)
      apply (rule trans)
       apply (rule Succ_Shift)
      apply (rule arg_cong[OF sym[OF append_Cons]])


     apply (rule ballI)
     apply (erule CollectE)
     apply (drule ShiftD)
     apply (drule bspec)
      apply (erule thin_rl)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (drule bspec)
      apply (rule CollectI)
      apply (erule subsetD[OF equalityD1[OF Succ_Shift]])
     apply (erule exE conjE)+
     apply (rule exI)
     apply (rule conjI)
      apply (rule trans[OF fun_cong[OF shift_def]])
      apply (rule trans[OF arg_cong[OF sym[OF append_Cons]]])
      apply assumption
     apply (rule conjI)
      apply (erule trans)
      apply (rule Collect_cong)
      apply (rule eqset_imp_iff)
      apply (rule sym)
      apply (rule trans)
       apply (rule Succ_Shift)
      apply (rule arg_cong[OF sym[OF append_Cons]])
     apply (erule trans)
     apply (rule Collect_cong)
     apply (rule eqset_imp_iff)
     apply (rule sym)
     apply (rule trans)
      apply (rule Succ_Shift)
     apply (rule arg_cong[OF sym[OF append_Cons]])

    apply (drule bspec)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule bspec)
     apply (erule subsetD[OF equalityD1])
     apply assumption
    apply (erule exE conjE)+
    apply (rule exI)
    apply (rule conjI)
     apply (rule trans[OF fun_cong[OF shift_def]])
     apply (erule trans[OF arg_cong[OF sym[OF append_Nil]]])
    apply (rule conjI)
     apply (erule trans)
     apply (rule Collect_cong)
     apply (rule eqset_imp_iff)
     apply (rule sym)
     apply (rule trans)
      apply (rule Succ_Shift)
     apply (rule arg_cong[OF sym[OF append_Nil]])
    apply (erule trans)
    apply (rule Collect_cong)
    apply (rule eqset_imp_iff)
    apply (rule sym)
    apply (rule trans)
     apply (rule Succ_Shift)
    apply (rule arg_cong[OF sym[OF append_Nil]])

   apply (rule ord_eq_le_trans[OF F1.set_map(3)])
   apply (rule image_subsetI)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (rule conjI)
    apply (rule conjI)
     apply (erule empty_Shift)
     apply (drule rev_subsetD)
      apply (erule equalityD1)
     apply (erule CollectD)
    apply (rule ballI)
    apply (rule conjI)
     apply (rule ballI)
     apply (erule CollectE)
     apply (drule ShiftD)
     apply (drule bspec)
      apply (erule thin_rl)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule bspec)
      apply (rule CollectI)
      apply (erule subsetD[OF equalityD1[OF Succ_Shift]])
     apply (erule exE conjE)+
     apply (rule exI)
     apply (rule conjI)
      apply (rule trans[OF fun_cong[OF shift_def]])
      apply (rule trans[OF arg_cong[OF sym[OF append_Cons]]])
      apply assumption
     apply (rule conjI)
      apply (erule trans)
      apply (rule Collect_cong)
      apply (rule eqset_imp_iff)
      apply (rule sym)
      apply (rule trans)
       apply (rule Succ_Shift)
      apply (rule arg_cong[OF sym[OF append_Cons]])
     apply (erule trans)
     apply (rule Collect_cong)
     apply (rule eqset_imp_iff)
     apply (rule sym)
     apply (rule trans)
      apply (rule Succ_Shift)
     apply (rule arg_cong[OF sym[OF append_Cons]])


    apply (rule ballI)
    apply (erule CollectE)
    apply (drule ShiftD)
    apply (drule bspec)
     apply (erule thin_rl)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule bspec)
     apply (rule CollectI)
     apply (erule subsetD[OF equalityD1[OF Succ_Shift]])
    apply (erule exE conjE)+
    apply (rule exI)
    apply (rule conjI)
     apply (rule trans[OF fun_cong[OF shift_def]])
     apply (rule trans[OF arg_cong[OF sym[OF append_Cons]]])
     apply assumption
    apply (rule conjI)
     apply (erule trans)
     apply (rule Collect_cong)
     apply (rule eqset_imp_iff)
     apply (rule sym)
     apply (rule trans)
      apply (rule Succ_Shift)
     apply (rule arg_cong[OF sym[OF append_Cons]])
    apply (erule trans)
    apply (rule Collect_cong)
    apply (rule eqset_imp_iff)
    apply (rule sym)
    apply (rule trans)
     apply (rule Succ_Shift)
    apply (rule arg_cong[OF sym[OF append_Cons]])

   apply (drule bspec)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule bspec)
    apply (erule subsetD[OF equalityD1])
    apply assumption
   apply (erule exE conjE)+
   apply (rule exI)
   apply (rule conjI)
    apply (rule trans[OF fun_cong[OF shift_def]])
    apply (erule trans[OF arg_cong[OF sym[OF append_Nil]]])
   apply (rule conjI)
    apply (erule trans)
    apply (rule Collect_cong)
    apply (rule eqset_imp_iff)
    apply (rule sym)
    apply (rule trans)
     apply (rule Succ_Shift)
    apply (rule arg_cong[OF sym[OF append_Nil]])
   apply (erule trans)
   apply (rule Collect_cong)
   apply (rule eqset_imp_iff)
   apply (rule sym)
   apply (rule trans)
    apply (rule Succ_Shift)
   apply (rule arg_cong[OF sym[OF append_Nil]])

(**)

  apply (rule ballI)
  apply (erule CollectE exE conjE)+
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (rule ssubst_mem[OF trans[OF fun_cong[OF strT2_def] prod.case]])
  apply (rule ssubst_mem)
   apply (rule trans)
    apply (erule arg_cong)
   apply (rule sum.case(2))
  apply (rule CollectI)
  apply (rule conjI)
   apply (rule subset_UNIV)
  apply (rule conjI)
   apply (rule ord_eq_le_trans[OF F2.set_map(2)])
   apply (rule image_subsetI)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (rule conjI)
    apply (rule conjI)
     apply (erule empty_Shift)
     apply (drule rev_subsetD)
      apply (erule equalityD1)
     apply (erule CollectD)
    apply (rule ballI)
    apply (rule conjI)
     apply (rule ballI)
     apply (erule CollectE)
     apply (drule ShiftD)
     apply (drule bspec)
      apply (erule thin_rl)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule bspec)
      apply (rule CollectI)
      apply (erule subsetD[OF equalityD1[OF Succ_Shift]])
     apply (erule exE conjE)+
     apply (rule exI)
     apply (rule conjI)
      apply (rule trans[OF fun_cong[OF shift_def]])
      apply (rule trans[OF arg_cong[OF sym[OF append_Cons]]])
      apply assumption
     apply (rule conjI)
      apply (erule trans)
      apply (rule Collect_cong)
      apply (rule eqset_imp_iff)
      apply (rule sym)
      apply (rule trans)
       apply (rule Succ_Shift)
      apply (rule arg_cong[OF sym[OF append_Cons]])
     apply (erule trans)
     apply (rule Collect_cong)
     apply (rule eqset_imp_iff)
     apply (rule sym)
     apply (rule trans)
      apply (rule Succ_Shift)
     apply (rule arg_cong[OF sym[OF append_Cons]])


    apply (rule ballI)
    apply (erule CollectE)
    apply (drule ShiftD)
    apply (drule bspec)
     apply (erule thin_rl)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule bspec)
     apply (rule CollectI)
     apply (erule subsetD[OF equalityD1[OF Succ_Shift]])
    apply (erule exE conjE)+
    apply (rule exI)
    apply (rule conjI)
     apply (rule trans[OF fun_cong[OF shift_def]])
     apply (rule trans[OF arg_cong[OF sym[OF append_Cons]]])
     apply assumption
    apply (rule conjI)
     apply (erule trans)
     apply (rule Collect_cong)
     apply (rule eqset_imp_iff)
     apply (rule sym)
     apply (rule trans)
      apply (rule Succ_Shift)
     apply (rule arg_cong[OF sym[OF append_Cons]])
    apply (erule trans)
    apply (rule Collect_cong)
    apply (rule eqset_imp_iff)
    apply (rule sym)
    apply (rule trans)
     apply (rule Succ_Shift)
    apply (rule arg_cong[OF sym[OF append_Cons]])

   apply (drule bspec)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (drule bspec)
    apply (erule subsetD[OF equalityD1])
    apply assumption
   apply (erule exE conjE)+
   apply (rule exI)
   apply (rule conjI)
    apply (rule trans[OF fun_cong[OF shift_def]])
    apply (erule trans[OF arg_cong[OF sym[OF append_Nil]]])
   apply (rule conjI)
    apply (erule trans)
    apply (rule Collect_cong)
    apply (rule eqset_imp_iff)
    apply (rule sym)
    apply (rule trans)
     apply (rule Succ_Shift)
    apply (rule arg_cong[OF sym[OF append_Nil]])
   apply (erule trans)
   apply (rule Collect_cong)
   apply (rule eqset_imp_iff)
   apply (rule sym)
   apply (rule trans)
    apply (rule Succ_Shift)
   apply (rule arg_cong[OF sym[OF append_Nil]])

  apply (rule ord_eq_le_trans[OF F2.set_map(3)])
  apply (rule image_subsetI)
  apply (rule CollectI)
  apply (rule exI)+
  apply (rule conjI)
   apply (rule refl)
  apply (rule conjI)
   apply (rule conjI)
    apply (erule empty_Shift)
    apply (drule rev_subsetD)
     apply (erule equalityD1)
    apply (erule CollectD)
   apply (rule ballI)
   apply (rule conjI)
    apply (rule ballI)
    apply (erule CollectE)
    apply (drule ShiftD)
    apply (drule bspec)
     apply (erule thin_rl)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule bspec)
     apply (rule CollectI)
     apply (erule subsetD[OF equalityD1[OF Succ_Shift]])
    apply (erule exE conjE)+
    apply (rule exI)
    apply (rule conjI)
     apply (rule trans[OF fun_cong[OF shift_def]])
     apply (rule trans[OF arg_cong[OF sym[OF append_Cons]]])
     apply assumption
    apply (rule conjI)
     apply (erule trans)
     apply (rule Collect_cong)
     apply (rule eqset_imp_iff)
     apply (rule sym)
     apply (rule trans)
      apply (rule Succ_Shift)
     apply (rule arg_cong[OF sym[OF append_Cons]])
    apply (erule trans)
    apply (rule Collect_cong)
    apply (rule eqset_imp_iff)
    apply (rule sym)
    apply (rule trans)
     apply (rule Succ_Shift)
    apply (rule arg_cong[OF sym[OF append_Cons]])


   apply (rule ballI)
   apply (erule CollectE)
   apply (drule ShiftD)
   apply (drule bspec)
    apply (erule thin_rl)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule bspec)
    apply (rule CollectI)
    apply (erule subsetD[OF equalityD1[OF Succ_Shift]])
   apply (erule exE conjE)+
   apply (rule exI)
   apply (rule conjI)
    apply (rule trans[OF fun_cong[OF shift_def]])
    apply (rule trans[OF arg_cong[OF sym[OF append_Cons]]])
    apply assumption
   apply (rule conjI)
    apply (erule trans)
    apply (rule Collect_cong)
    apply (rule eqset_imp_iff)
    apply (rule sym)
    apply (rule trans)
     apply (rule Succ_Shift)
    apply (rule arg_cong[OF sym[OF append_Cons]])
   apply (erule trans)
   apply (rule Collect_cong)
   apply (rule eqset_imp_iff)
   apply (rule sym)
   apply (rule trans)
    apply (rule Succ_Shift)
   apply (rule arg_cong[OF sym[OF append_Cons]])

  apply (drule bspec)
   apply assumption
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (drule bspec)
   apply (erule subsetD[OF equalityD1])
   apply assumption
  apply (erule exE conjE)+
  apply (rule exI)
  apply (rule conjI)
   apply (rule trans[OF fun_cong[OF shift_def]])
   apply (erule trans[OF arg_cong[OF sym[OF append_Nil]]])
  apply (rule conjI)
   apply (erule trans)
   apply (rule Collect_cong)
   apply (rule eqset_imp_iff)
   apply (rule sym)
   apply (rule trans)
    apply (rule Succ_Shift)
   apply (rule arg_cong[OF sym[OF append_Nil]])
  apply (erule trans)
  apply (rule Collect_cong)
  apply (rule eqset_imp_iff)
  apply (rule sym)
  apply (rule trans)
   apply (rule Succ_Shift)
  apply (rule arg_cong[OF sym[OF append_Nil]])
  done

abbreviation tobd_F12 where "tobd_F12 s1 x ≡ toCard (F1set2 (s1 x)) bd_F"
abbreviation tobd_F13 where "tobd_F13 s1 x ≡ toCard (F1set3 (s1 x)) bd_F"
abbreviation tobd_F22 where "tobd_F22 s2 x ≡ toCard (F2set2 (s2 x)) bd_F"
abbreviation tobd_F23 where "tobd_F23 s2 x ≡ toCard (F2set3 (s2 x)) bd_F"
abbreviation frombd_F12 where "frombd_F12 s1 x ≡ fromCard (F1set2 (s1 x)) bd_F"
abbreviation frombd_F13 where "frombd_F13 s1 x ≡ fromCard (F1set3 (s1 x)) bd_F"
abbreviation frombd_F22 where "frombd_F22 s2 x ≡ fromCard (F2set2 (s2 x)) bd_F"
abbreviation frombd_F23 where "frombd_F23 s2 x ≡ fromCard (F2set3 (s2 x)) bd_F"

lemmas tobd_F12_inj = toCard_inj[OF ordLess_imp_ordLeq[OF F1set2_bd'] bd_F_Card_order]
lemmas tobd_F13_inj = toCard_inj[OF ordLess_imp_ordLeq[OF F1set3_bd'] bd_F_Card_order]
lemmas tobd_F22_inj = toCard_inj[OF ordLess_imp_ordLeq[OF F2set2_bd'] bd_F_Card_order]
lemmas tobd_F23_inj = toCard_inj[OF ordLess_imp_ordLeq[OF F2set3_bd'] bd_F_Card_order]
lemmas frombd_F12_tobd_F12 = fromCard_toCard[OF ordLess_imp_ordLeq[OF F1set2_bd'] bd_F_Card_order]
lemmas frombd_F13_tobd_F13 = fromCard_toCard[OF ordLess_imp_ordLeq[OF F1set3_bd'] bd_F_Card_order]
lemmas frombd_F22_tobd_F22 = fromCard_toCard[OF ordLess_imp_ordLeq[OF F2set2_bd'] bd_F_Card_order]
lemmas frombd_F23_tobd_F23 = fromCard_toCard[OF ordLess_imp_ordLeq[OF F2set3_bd'] bd_F_Card_order]

(* the levels of the behavior of a via s, through the embedding in Field bd_F *)
definition Lev where
  "Lev s1 s2 = rec_nat (%a. {[]}, %b. {[]})
    (%n rec.
      (%a1.
        {Inl (tobd_F12 s1 a1 b1) # kl | b1 kl. b1 ∈ F1set2 (s1 a1) ∧ kl ∈ fst rec b1} ∪
        {Inr (tobd_F13 s1 a1 b2) # kl | b2 kl. b2 ∈ F1set3 (s1 a1) ∧ kl ∈ snd rec b2},
       %a2.
        {Inl (tobd_F22 s2 a2 b1) # kl | b1 kl. b1 ∈ F2set2 (s2 a2) ∧ kl ∈ fst rec b1} ∪
        {Inr (tobd_F23 s2 a2 b2) # kl | b2 kl. b2 ∈ F2set3 (s2 a2) ∧ kl ∈ snd rec b2}))"

abbreviation Lev1 where "Lev1 s1 s2 n ≡ fst (Lev s1 s2 n)"
abbreviation Lev2 where "Lev2 s1 s2 n ≡ snd (Lev s1 s2 n)"

lemmas Lev1_0 = fun_cong[OF fstI[OF rec_nat_0_imp[OF Lev_def]]]
lemmas Lev2_0 = fun_cong[OF sndI[OF rec_nat_0_imp[OF Lev_def]]]
lemmas Lev1_Suc = fun_cong[OF fstI[OF rec_nat_Suc_imp[OF Lev_def]]]
lemmas Lev2_Suc = fun_cong[OF sndI[OF rec_nat_Suc_imp[OF Lev_def]]]

(* recovery of the element corresponding to a path: *)
definition rv where
  "rv s1 s2 = rec_list (%b1. Inl b1, %b2. Inr b2)
    (%k kl rec.
      (%b1. case_sum (%k1. fst rec (frombd_F12 s1 b1 k1)) (%k2. snd rec (frombd_F13 s1 b1 k2)) k,
       %b2. case_sum (%k1. fst rec (frombd_F22 s2 b2 k1)) (%k2. snd rec (frombd_F23 s2 b2 k2)) k))"

abbreviation rv1 where "rv1 s1 s2 kl ≡ fst (rv s1 s2 kl)"
abbreviation rv2 where "rv2 s1 s2 kl ≡ snd (rv s1 s2 kl)"

lemmas rv1_Nil = fun_cong[OF fstI[OF rec_list_Nil_imp[OF rv_def]]]
lemmas rv2_Nil = fun_cong[OF sndI[OF rec_list_Nil_imp[OF rv_def]]]
lemmas rv1_Cons = fun_cong[OF fstI[OF rec_list_Cons_imp[OF rv_def]]]
lemmas rv2_Cons = fun_cong[OF sndI[OF rec_list_Cons_imp[OF rv_def]]]

(* the labels: *)
abbreviation "Lab1 s1 s2 b1 kl ≡
  (case_sum (%k. Inl (F1map id (tobd_F12 s1 k) (tobd_F13 s1 k) (s1 k)))
                (%k. Inr (F2map id (tobd_F22 s2 k) (tobd_F23 s2 k) (s2 k))) (rv1 s1 s2 kl b1))"

abbreviation "Lab2 s1 s2 b2 kl ≡
  (case_sum (%k. Inl (F1map id (tobd_F12 s1 k) (tobd_F13 s1 k) (s1 k)))
                (%k. Inr (F2map id (tobd_F22 s2 k) (tobd_F23 s2 k) (s2 k))) (rv2 s1 s2 kl b2))"

(* the behavior of a under s: *)
definition "beh1 s1 s2 a = (∪n. Lev1 s1 s2 n a, Lab1 s1 s2 a)"
definition "beh2 s1 s2 a = (∪n. Lev2 s1 s2 n a, Lab2 s1 s2 a)"

lemma length_Lev:
  "∀kl b1 b2. (kl ∈ Lev1 s1 s2 n b1 ⟶ length kl = n) ∧
              (kl ∈ Lev2 s1 s2 n b2 ⟶ length kl = n)"
  apply (rule nat_induct)
   apply (rule allI)+
   apply (rule conjI)
    apply (rule impI)
    apply (drule subsetD[OF equalityD1[OF Lev1_0]])
    apply (erule singletonE)
    apply (erule ssubst)
    apply (rule list.size(3))

   apply (rule impI)
   apply (drule subsetD[OF equalityD1[OF Lev2_0]])
   apply (erule singletonE)
   apply (erule ssubst)
   apply (rule list.size(3))

  apply (rule allI)+
  apply (rule conjI)
   apply (rule impI)
   apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
   apply (erule UnE)
    apply (erule CollectE exE conjE)+
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (rule trans)
     apply (rule length_Cons)
    apply (rule arg_cong[of _ _ Suc])
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule mp)
    apply assumption

   apply (erule CollectE exE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule trans)
    apply (rule length_Cons)
   apply (rule arg_cong[of _ _ Suc])
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule mp)
   apply assumption


  apply (rule impI)
  apply (drule subsetD[OF equalityD1[OF Lev2_Suc]])
  apply (erule UnE)
   apply (erule CollectE exE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule trans)
    apply (rule length_Cons)
   apply (rule arg_cong[of _ _ Suc])
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (erule mp)
   apply assumption

  apply (erule CollectE exE conjE)+
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (rule trans)
   apply (rule length_Cons)
  apply (rule arg_cong[of _ _ Suc])
  apply (erule allE)+
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (erule mp)
  apply assumption
  done

lemmas length_Lev1 = mp[OF conjunct1[OF spec[OF spec [OF spec[OF length_Lev]]]]]
lemmas length_Lev2 = mp[OF conjunct2[OF spec[OF spec [OF spec[OF length_Lev]]]]]

lemma length_Lev1': "kl ∈ Lev1 s1 s2 n a ==> kl ∈ Lev1 s1 s2 (length kl) a"
  apply (frule length_Lev1)
  apply (erule ssubst)
  apply assumption
  done

lemma length_Lev2': "kl ∈ Lev2 s1 s2 n a ==> kl ∈ Lev2 s1 s2 (length kl) a"
  apply (frule length_Lev2)
  apply (erule ssubst)
  apply assumption
  done

lemma rv_last:
  "∀k b1 b2.
   ((∃b1'. rv1 s1 s2 (kl @ [Inl k]) b1 = Inl b1') ∧
    (∃b1'. rv1 s1 s2 (kl @ [Inr k]) b1 = Inr b1')) ∧
   ((∃b2'. rv2 s1 s2 (kl @ [Inl k]) b2 = Inl b2') ∧
    (∃b2'. rv2 s1 s2 (kl @ [Inr k]) b2 = Inr b2'))"
  apply (rule list.induct[of _ kl])
   apply (rule allI)+
   apply (rule conjI)
    apply (rule conjI)
     apply (rule exI)
     apply (rule trans[OF arg_cong[OF append_Nil]])
     apply (rule trans[OF rv1_Cons])
     apply (rule trans[OF arg_cong[OF sum.case(1)]])
     apply (rule rv1_Nil)
    apply (rule exI)
    apply (rule trans[OF arg_cong[OF append_Nil]])
    apply (rule trans[OF rv1_Cons])
    apply (rule trans[OF arg_cong[OF sum.case(2)]])
    apply (rule rv2_Nil)
   apply (rule conjI)
    apply (rule exI)
    apply (rule trans[OF arg_cong[OF append_Nil]])
    apply (rule trans[OF rv2_Cons])
    apply (rule trans[OF arg_cong[OF sum.case(1)]])
    apply (rule rv1_Nil)
   apply (rule exI)
   apply (rule trans[OF arg_cong[OF append_Nil]])
   apply (rule trans[OF rv2_Cons])
   apply (rule trans[OF arg_cong[OF sum.case(2)]])
   apply (rule rv2_Nil)

  apply (rule allI)+
  apply (rule sum.exhaust)
   apply (rule conjI)
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (rule conjI)
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (erule exE)
     apply (rule exI)
     apply (rule trans[OF arg_cong[OF append_Cons]])
     apply (rule trans[OF rv1_Cons])
     apply (erule trans[OF arg_cong[OF sum.case_cong_weak]])
     apply (rule trans[OF arg_cong[OF sum.case(1)]])
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (erule exE)
    apply (rule exI)
    apply (rule trans[OF arg_cong[OF append_Cons]])
    apply (rule trans[OF rv1_Cons])
    apply (erule trans[OF arg_cong[OF sum.case_cong_weak]])
    apply (rule trans[OF arg_cong[OF sum.case(1)]])
    apply assumption

   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (rule conjI)
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule exE)
    apply (rule exI)
    apply (rule trans[OF arg_cong[OF append_Cons]])
    apply (rule trans[OF rv2_Cons])
    apply (erule trans[OF arg_cong[OF sum.case_cong_weak]])
    apply (rule trans[OF arg_cong[OF sum.case(1)]])
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule exE)
   apply (rule exI)
   apply (rule trans[OF arg_cong[OF append_Cons]])
   apply (rule trans[OF rv2_Cons])
   apply (erule trans[OF arg_cong[OF sum.case_cong_weak]])
   apply (rule trans[OF arg_cong[OF sum.case(1)]])
   apply assumption

  apply (rule conjI)
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (rule conjI)
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule exE)
    apply (rule exI)
    apply (rule trans[OF arg_cong[OF append_Cons]])
    apply (rule trans[OF rv1_Cons])
    apply (erule trans[OF arg_cong[OF sum.case_cong_weak]])
    apply (rule trans[OF arg_cong[OF sum.case(2)]])
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule exE)
   apply (rule exI)
   apply (rule trans[OF arg_cong[OF append_Cons]])
   apply (rule trans[OF rv1_Cons])
   apply (erule trans[OF arg_cong[OF sum.case_cong_weak]])
   apply (rule trans[OF arg_cong[OF sum.case(2)]])
   apply assumption

  apply (erule allE)+
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (rule conjI)
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (erule exE)
   apply (rule exI)
   apply (rule trans[OF arg_cong[OF append_Cons]])
   apply (rule trans[OF rv2_Cons])
   apply (erule trans[OF arg_cong[OF sum.case_cong_weak]])
   apply (rule trans[OF arg_cong[OF sum.case(2)]])
   apply assumption
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (erule exE)
  apply (rule exI)
  apply (rule trans[OF arg_cong[OF append_Cons]])
  apply (rule trans[OF rv2_Cons])
  apply (erule trans[OF arg_cong[OF sum.case_cong_weak]])
  apply (rule trans[OF arg_cong[OF sum.case(2)]])
  apply assumption
  done

lemmas rv_last' = spec[OF spec[OF spec[OF rv_last]]]
lemmas rv1_Inl_last = conjunct1[OF conjunct1[OF rv_last']]
lemmas rv1_Inr_last = conjunct2[OF conjunct1[OF rv_last']]
lemmas rv2_Inl_last = conjunct1[OF conjunct2[OF rv_last']]
lemmas rv2_Inr_last = conjunct2[OF conjunct2[OF rv_last']]

lemma Fset_Lev:
  "∀kl b1 b2 b1' b2' b1'' b2''.
   (kl ∈ Lev1 s1 s2 n b1 ⟶
    ((rv1 s1 s2 kl b1 = Inl b1' ⟶
      (b1'' ∈ F1set2 (s1 b1') ⟶
        kl @ [Inl (tobd_F12 s1 b1' b1'')] ∈ Lev1 s1 s2 (Suc n) b1) ∧
      (b2'' ∈ F1set3 (s1 b1') ⟶
        kl @ [Inr (tobd_F13 s1 b1' b2'')] ∈ Lev1 s1 s2 (Suc n) b1)) ∧
     (rv1 s1 s2 kl b1 = Inr b2' ⟶
      (b1'' ∈ F2set2 (s2 b2') ⟶
        kl @ [Inl (tobd_F22 s2 b2' b1'')] ∈ Lev1 s1 s2 (Suc n) b1) ∧
      (b2'' ∈ F2set3 (s2 b2') ⟶
        kl @ [Inr (tobd_F23 s2 b2' b2'')] ∈ Lev1 s1 s2 (Suc n) b1)))) ∧
   (kl ∈ Lev2 s1 s2 n b2 ⟶
    ((rv2 s1 s2 kl b2 = Inl b1' ⟶
      (b1'' ∈ F1set2 (s1 b1') ⟶
        kl @ [Inl (tobd_F12 s1 b1' b1'')] ∈ Lev2 s1 s2 (Suc n) b2) ∧
      (b2'' ∈ F1set3 (s1 b1') ⟶
        kl @ [Inr (tobd_F13 s1 b1' b2'')] ∈ Lev2 s1 s2 (Suc n) b2)) ∧
     (rv2 s1 s2 kl b2 = Inr b2' ⟶
      (b1'' ∈ F2set2 (s2 b2') ⟶
        kl @ [Inl (tobd_F22 s2 b2' b1'')] ∈ Lev2 s1 s2 (Suc n) b2) ∧
      (b2'' ∈ F2set3 (s2 b2') ⟶
        kl @ [Inr (tobd_F23 s2 b2' b2'')] ∈ Lev2 s1 s2 (Suc n) b2))))"
  apply (rule nat_induct[of _ n])
    (*IB*)
   apply (rule allI)+
   apply (rule conjI)
    apply (rule impI)
    apply (drule subsetD[OF equalityD1[OF Lev1_0]])
    apply (erule singletonE)
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (rule conjI)
     apply (rule impI)
     apply (drule trans[OF sym])
      apply (rule rv1_Nil)
     apply (drule Inl_inject)
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (rule conjI)
      apply (rule impI)
      apply (rule ssubst_mem[OF append_Nil])
      apply (rule subsetD[OF equalityD2])
       apply (rule Lev1_Suc)
      apply (rule UnI1)
      apply (rule CollectI)
      apply (rule exI)+
      apply (rule conjI)
       apply (rule refl)
      apply (erule conjI)
      apply (rule subsetD[OF equalityD2])
       apply (rule Lev1_0)
      apply (rule singletonI)
     apply (rule impI)
     apply (rule ssubst_mem[OF append_Nil])
     apply (rule subsetD[OF equalityD2])
      apply (rule Lev1_Suc)
     apply (rule UnI2)
     apply (rule CollectI)
     apply (rule exI)+
     apply (rule conjI)
      apply (rule refl)
     apply (erule conjI)
     apply (rule subsetD[OF equalityD2])
      apply (rule Lev2_0)
     apply (rule singletonI)

    apply (rule impI)
    apply (drule trans[OF sym])
     apply (rule rv1_Nil)
    apply (erule notE[OF Inr_not_Inl])

   apply (rule impI)
   apply (drule rev_subsetD[OF _ equalityD1])
    apply (rule Lev2_0)
   apply (erule singletonE)
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule conjI)
    apply (rule impI)
    apply (drule trans[OF sym])
     apply (rule rv2_Nil)
    apply (erule notE[OF Inl_not_Inr])

   apply (rule impI)
   apply (drule trans[OF sym])
    apply (rule rv2_Nil)
   apply (drule Inr_inject)
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (tactic ‹stac @{context} @{thm append_Nil} 1›)+
   apply (rule conjI)
    apply (rule impI)
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev2_Suc)
    apply (rule UnI1)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (erule conjI)
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev1_0)
    apply (rule singletonI)
   apply (rule impI)
   apply (rule subsetD[OF equalityD2])
    apply (rule Lev2_Suc)
   apply (rule UnI2)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (erule conjI)
   apply (rule subsetD[OF equalityD2])
    apply (rule Lev2_0)
   apply (rule singletonI)

(*IS*)
  apply (rule allI)+
  apply (rule conjI)
   apply (rule impI)
   apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
   apply (erule UnE)
    apply (erule CollectE exE conjE)+
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (rule conjI)
     apply (rule impI)
     apply (rule conjI)
      apply (rule impI)
      apply (rule subsetD[OF equalityD2])
       apply (rule Lev1_Suc)
      apply (rule ssubst_mem[OF append_Cons])
      apply (rule UnI1)
      apply (rule CollectI)
      apply (rule exI)+
      apply (rule conjI)
       apply (rule refl)
      apply (rule conjI)
       apply assumption
      apply (drule sym[OF trans[OF sym]])
       apply (rule trans[OF rv1_Cons])
       apply (rule trans[OF sum.case(1)])
       apply (erule arg_cong[OF frombd_F12_tobd_F12])
      apply (erule allE)+
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (drule mp)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (drule mp)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (erule mp)
      apply assumption

     apply (rule impI)
     apply (rule subsetD[OF equalityD2])
      apply (rule Lev1_Suc)
     apply (rule ssubst_mem[OF append_Cons])
     apply (rule UnI1)
     apply (rule CollectI)
     apply (rule exI)+
     apply (rule conjI)
      apply (rule refl)
     apply (rule conjI)
      apply assumption
     apply (drule sym[OF trans[OF sym]])
      apply (rule trans[OF rv1_Cons])
      apply (rule trans[OF sum.case(1)])
      apply (erule arg_cong[OF frombd_F12_tobd_F12])
     apply (erule allE)+
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (erule mp)
     apply assumption

    apply (rule impI)
    apply (rule conjI)
     apply (rule impI)
     apply (rule subsetD[OF equalityD2])
      apply (rule Lev1_Suc)
     apply (rule ssubst_mem[OF append_Cons])
     apply (rule UnI1)
     apply (rule CollectI)
     apply (rule exI)+
     apply (rule conjI)
      apply (rule refl)
     apply (rule conjI)
      apply assumption
     apply (drule sym[OF trans[OF sym]])
      apply (rule trans[OF rv1_Cons])
      apply (rule trans[OF sum.case(1)])
      apply (erule arg_cong[OF frombd_F12_tobd_F12])
     apply (erule allE)+
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (erule mp)
     apply assumption

    apply (rule impI)
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev1_Suc)
    apply (rule ssubst_mem[OF append_Cons])
    apply (rule UnI1)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (rule conjI)
     apply assumption
    apply (drule sym[OF trans[OF sym]])
     apply (rule trans[OF rv1_Cons])
     apply (rule trans[OF sum.case(1)])
     apply (erule arg_cong[OF frombd_F12_tobd_F12])
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (erule mp)
    apply assumption
    (*UN1/2*)
   apply (erule CollectE exE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (tactic ‹stac @{context} @{thm rv1_Cons} 1›)
   apply (tactic ‹stac @{context} @{thm sum.case(2)} 1›)
   apply (tactic ‹stac @{context} @{thm frombd_F13_tobd_F13} 1›)
    apply assumption
   apply (rule conjI)
    apply (rule impI)
    apply (rule conjI)
     apply (rule impI)
     apply (rule subsetD[OF equalityD2])
      apply (rule Lev1_Suc)
     apply (rule ssubst_mem[OF append_Cons])
     apply (rule UnI2)
     apply (rule CollectI)
     apply (rule exI)+
     apply (rule conjI)
      apply (rule refl)
     apply (erule conjI)
     apply (erule allE)+
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (erule mp)
     apply assumption

    apply (rule impI)
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev1_Suc)
    apply (rule ssubst_mem[OF append_Cons])
    apply (rule UnI2)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (erule conjI)
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (erule mp)
    apply assumption

   apply (rule impI)
   apply (rule conjI)
    apply (rule impI)
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev1_Suc)
    apply (rule ssubst_mem[OF append_Cons])
    apply (rule UnI2)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (erule conjI)
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule mp)
    apply assumption

   apply (rule impI)
   apply (rule subsetD[OF equalityD2])
    apply (rule Lev1_Suc)
   apply (rule ssubst_mem[OF append_Cons])
   apply (rule UnI2)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (erule conjI)
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule mp)
   apply assumption

(**)

  apply (rule impI)
  apply (drule rev_subsetD[OF _ equalityD1])
   apply (rule Lev2_Suc)
  apply (erule UnE)
   apply (erule CollectE exE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (tactic ‹stac @{context} @{thm rv2_Cons} 1›)
   apply (tactic ‹stac @{context} @{thm sum.case(1)} 1›)
   apply (tactic ‹stac @{context} @{thm frombd_F22_tobd_F22} 1›)
    apply assumption
   apply (rule conjI)
    apply (rule impI)
    apply (rule conjI)
     apply (rule impI)
     apply (rule subsetD[OF equalityD2])
      apply (rule Lev2_Suc)
     apply (rule ssubst_mem[OF append_Cons])
     apply (rule UnI1)
     apply (rule CollectI)
     apply (rule exI)+
     apply (rule conjI)
      apply (rule refl)
     apply (erule conjI)
     apply (erule allE)+
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (erule mp)
     apply assumption

    apply (rule impI)
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev2_Suc)
    apply (rule ssubst_mem[OF append_Cons])
    apply (rule UnI1)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (erule conjI)
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (erule mp)
    apply assumption

   apply (rule impI)
   apply (rule conjI)
    apply (rule impI)
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev2_Suc)
    apply (rule ssubst_mem[OF append_Cons])
    apply (rule UnI1)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (erule conjI)
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule mp)
    apply assumption

   apply (rule impI)
   apply (rule subsetD[OF equalityD2])
    apply (rule Lev2_Suc)
   apply (rule ssubst_mem[OF append_Cons])
   apply (rule UnI1)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (erule conjI)
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule mp)
   apply assumption
    (*UN1/2*)
  apply (erule CollectE exE conjE)+
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (tactic ‹stac @{context} @{thm rv2_Cons} 1›)
  apply (tactic ‹stac @{context} @{thm sum.case(2)} 1›)
  apply (tactic ‹stac @{context} @{thm frombd_F23_tobd_F23} 1›)
   apply assumption
  apply (rule conjI)
   apply (rule impI)
   apply (rule conjI)
    apply (rule impI)
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev2_Suc)
    apply (rule ssubst_mem[OF append_Cons])
    apply (rule UnI2)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (erule conjI)
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule mp)
    apply assumption

   apply (rule impI)
   apply (rule subsetD[OF equalityD2])
    apply (rule Lev2_Suc)
   apply (rule ssubst_mem[OF append_Cons])
   apply (rule UnI2)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (erule conjI)
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule mp)
   apply assumption

  apply (rule impI)
  apply (rule conjI)
   apply (rule impI)
   apply (rule subsetD[OF equalityD2])
    apply (rule Lev2_Suc)
   apply (rule ssubst_mem[OF append_Cons])
   apply (rule UnI2)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (erule conjI)
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (erule mp)
   apply assumption

  apply (rule impI)
  apply (rule subsetD[OF equalityD2])
   apply (rule Lev2_Suc)
  apply (rule ssubst_mem[OF append_Cons])
  apply (rule UnI2)
  apply (rule CollectI)
  apply (rule exI)+
  apply (rule conjI)
   apply (rule refl)
  apply (erule conjI)
  apply (erule allE)+
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (drule mp)
   apply assumption
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (drule mp)
   apply assumption
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (erule mp)
  apply assumption
  done

lemmas Fset_Lev' = spec[OF spec[OF spec[OF spec[OF spec[OF spec[OF spec[OF Fset_Lev]]]]]]]
lemmas F1set2_Lev1 = mp[OF conjunct1[OF mp[OF conjunct1[OF mp[OF conjunct1[OF Fset_Lev']]]]]]
lemmas F1set2_Lev2 = mp[OF conjunct1[OF mp[OF conjunct1[OF mp[OF conjunct2[OF Fset_Lev']]]]]]
lemmas F2set2_Lev1 = mp[OF conjunct1[OF mp[OF conjunct2[OF mp[OF conjunct1[OF Fset_Lev']]]]]]
lemmas F2set2_Lev2 = mp[OF conjunct1[OF mp[OF conjunct2[OF mp[OF conjunct2[OF Fset_Lev']]]]]]
lemmas F1set3_Lev1 = mp[OF conjunct2[OF mp[OF conjunct1[OF mp[OF conjunct1[OF Fset_Lev']]]]]]
lemmas F1set3_Lev2 = mp[OF conjunct2[OF mp[OF conjunct1[OF mp[OF conjunct2[OF Fset_Lev']]]]]]
lemmas F2set3_Lev1 = mp[OF conjunct2[OF mp[OF conjunct2[OF mp[OF conjunct1[OF Fset_Lev']]]]]]
lemmas F2set3_Lev2 = mp[OF conjunct2[OF mp[OF conjunct2[OF mp[OF conjunct2[OF Fset_Lev']]]]]]

lemma Fset_image_Lev:
  "∀kl k b1 b2 b1' b2'.
   (kl ∈ Lev1 s1 s2 n b1 ⟶
    (kl @ [Inl k] ∈ Lev1 s1 s2 (Suc n) b1 ⟶
      (rv1 s1 s2 kl b1 = Inl b1' ⟶ k ∈ tobd_F12 s1 b1' ` F1set2 (s1 b1')) ∧
      (rv1 s1 s2 kl b1 = Inr b2' ⟶ k ∈ tobd_F22 s2 b2' ` F2set2 (s2 b2'))) ∧
    (kl @ [Inr k] ∈ Lev1 s1 s2 (Suc n) b1 ⟶
      (rv1 s1 s2 kl b1 = Inl b1' ⟶ k ∈ tobd_F13 s1 b1' ` F1set3 (s1 b1')) ∧
      (rv1 s1 s2 kl b1 = Inr b2' ⟶ k ∈ tobd_F23 s2 b2' ` F2set3 (s2 b2')))) ∧
   (kl ∈ Lev2 s1 s2 n b2 ⟶
    (kl @ [Inl k] ∈ Lev2 s1 s2 (Suc n) b2 ⟶
      (rv2 s1 s2 kl b2 = Inl b1' ⟶ k ∈ tobd_F12 s1 b1' ` F1set2 (s1 b1')) ∧
      (rv2 s1 s2 kl b2 = Inr b2' ⟶ k ∈ tobd_F22 s2 b2' ` F2set2 (s2 b2'))) ∧
    (kl @ [Inr k] ∈ Lev2 s1 s2 (Suc n) b2 ⟶
      (rv2 s1 s2 kl b2 = Inl b1' ⟶ k ∈ tobd_F13 s1 b1' ` F1set3 (s1 b1')) ∧
      (rv2 s1 s2 kl b2 = Inr b2' ⟶ k ∈ tobd_F23 s2 b2' ` F2set3 (s2 b2'))))"
  apply (rule nat_induct[of _ n])
    (*IB*)
   apply (rule allI)+
   apply (rule conjI)
    apply (rule impI)
    apply (drule subsetD[OF equalityD1[OF Lev1_0]])
    apply (erule singletonE)
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (rule conjI)
     apply (rule impI)
     apply (rule conjI)
      apply (rule impI)
      apply (drule trans[OF sym])
       apply (rule rv1_Nil)
      apply (drule ssubst_mem[OF sym[OF append_Nil]])
      apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
      apply (drule Inl_inject)
      apply (tactic ‹hyp_subst_tac @{context} 1›)
      apply (erule UnE)
       apply (erule CollectE exE conjE)+
       apply (drule list.inject[THEN iffD1])
       apply (erule conjE)
       apply (drule Inl_inject)
       apply (tactic ‹hyp_subst_tac @{context} 1›)
       apply (erule imageI)
      apply (erule CollectE exE conjE)+
      apply (drule list.inject[THEN iffD1])
      apply (erule conjE)
      apply (erule notE[OF Inl_not_Inr])
     apply (rule impI)
     apply (drule trans[OF sym])
      apply (rule rv1_Nil)
     apply (erule notE[OF Inr_not_Inl])

    apply (rule impI)
    apply (rule conjI)
     apply (rule impI)
     apply (drule ssubst_mem[OF sym[OF append_Nil]])
     apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
     apply (drule trans[OF sym])
      apply (rule rv1_Nil)
     apply (drule Inl_inject)
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (erule UnE)
      apply (erule CollectE exE conjE)+
      apply (drule list.inject[THEN iffD1])
      apply (erule conjE)
      apply (erule notE[OF Inr_not_Inl])
     apply (erule CollectE exE conjE)+
     apply (drule list.inject[THEN iffD1])
     apply (erule conjE)
     apply (drule Inr_inject)
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (erule imageI)
    apply (rule impI)
    apply (drule trans[OF sym])
     apply (rule rv1_Nil)
    apply (erule notE[OF Inr_not_Inl])

   apply (rule impI)
   apply (drule subsetD[OF equalityD1[OF Lev2_0]])
   apply (erule singletonE)
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule conjI)
    apply (rule impI)
    apply (rule conjI)
     apply (rule impI)
     apply (drule trans[OF sym])
      apply (rule rv2_Nil)
     apply (erule notE[OF Inl_not_Inr])
    apply (rule impI)
    apply (drule ssubst_mem[OF sym[OF append_Nil]])
    apply (drule subsetD[OF equalityD1[OF Lev2_Suc]])
    apply (drule trans[OF sym])
     apply (rule rv2_Nil)
    apply (drule Inr_inject)
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (erule UnE)
     apply (erule CollectE exE conjE)+
     apply (drule list.inject[THEN iffD1])
     apply (erule conjE)
     apply (drule Inl_inject)
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (erule imageI)
    apply (erule CollectE exE conjE)+
    apply (drule list.inject[THEN iffD1])
    apply (erule conjE)
    apply (erule notE[OF Inl_not_Inr])

   apply (rule impI)
   apply (rule conjI)
    apply (rule impI)
    apply (drule trans[OF sym])
     apply (rule rv2_Nil)
    apply (erule notE[OF Inl_not_Inr])
   apply (rule impI)
   apply (drule ssubst_mem[OF sym[OF append_Nil]])
   apply (drule subsetD[OF equalityD1[OF Lev2_Suc]])
   apply (drule trans[OF sym])
    apply (rule rv2_Nil)
   apply (drule Inr_inject)
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (erule UnE)
    apply (erule CollectE exE conjE)+
    apply (drule list.inject[THEN iffD1])
    apply (erule conjE)
    apply (erule notE[OF Inr_not_Inl])
   apply (erule CollectE exE conjE)+
   apply (drule list.inject[THEN iffD1])
   apply (erule conjE)
   apply (drule Inr_inject)
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (erule imageI)

(*IS*)

  apply (rule allI)+
  apply (rule conjI)
   apply (rule impI)
   apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
   apply (erule UnE)
    apply (erule CollectE exE conjE)+
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (rule conjI)
     apply (rule impI)
     apply (drule ssubst_mem[OF sym[OF append_Cons]])
     apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
     apply (erule UnE)
      apply (erule CollectE exE conjE)+
      apply (drule list.inject[THEN iffD1])
      apply (erule conjE)
      apply (drule Inl_inject)
      apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 (@{thm tobd_F12_inj} RS iffD1)) 1›)
        apply assumption
       apply assumption
      apply (tactic ‹hyp_subst_tac @{context} 1›)
      apply (rule conjI)
       apply (rule impI)
       apply (drule trans[OF sym])
        apply (rule trans[OF rv1_Cons])
        apply (rule trans[OF arg_cong[OF sum.case(1)]])
        apply (erule arg_cong[OF frombd_F12_tobd_F12])
       apply (erule allE)+
       apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
       apply (drule mp)
        apply assumption
       apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
       apply (drule mp)
        apply assumption
       apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
       apply (erule mp)
       apply (erule sym)

      apply (rule impI)
      apply (drule trans[OF sym])
       apply (rule trans[OF rv1_Cons])
       apply (rule trans[OF arg_cong[OF sum.case(1)]])
       apply (erule arg_cong[OF frombd_F12_tobd_F12])
      apply (erule allE)+
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (drule mp)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (drule mp)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
      apply (erule mp)
      apply (erule sym)

     apply (erule CollectE exE conjE)+
     apply (drule list.inject[THEN iffD1])
     apply (erule conjE)
     apply (erule notE[OF Inl_not_Inr])

    apply (rule impI)
    apply (drule ssubst_mem[OF sym[OF append_Cons]])
    apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
    apply (erule UnE)
     apply (erule CollectE exE conjE)+
     apply (drule list.inject[THEN iffD1])
     apply (erule conjE)
     apply (drule Inl_inject)
     apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F12_inj[THEN iffD1]}) 1›)
       apply assumption
      apply assumption
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (rule conjI)
      apply (rule impI)
      apply (drule trans[OF sym])
       apply (rule trans[OF rv1_Cons])
       apply (rule trans[OF arg_cong[OF sum.case(1)]])
       apply (erule arg_cong[OF frombd_F12_tobd_F12])
      apply (erule allE)+
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (drule mp)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
      apply (drule mp)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (erule mp)
      apply (erule sym)

     apply (rule impI)
     apply (drule trans[OF sym])
      apply (rule trans[OF rv1_Cons])
      apply (rule trans[OF arg_cong[OF sum.case(1)]])
      apply (erule arg_cong[OF frombd_F12_tobd_F12])
     apply (erule allE)+
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (erule mp)
     apply (erule sym)

    apply (erule CollectE exE conjE)+
    apply (drule list.inject[THEN iffD1])
    apply (erule conjE)
    apply (erule notE[OF Inl_not_Inr])
    (*outer UN1/2*)
   apply (erule CollectE exE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule conjI)
    apply (rule impI)
    apply (drule ssubst_mem[OF sym[OF append_Cons]])
    apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
    apply (erule UnE)
     apply (erule CollectE exE conjE)+
     apply (drule list.inject[THEN iffD1])
     apply (erule conjE)
     apply (erule notE[OF Inr_not_Inl])

    apply (erule CollectE exE conjE)+
    apply (drule list.inject[THEN iffD1])
    apply (erule conjE)
    apply (drule Inr_inject)
    apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F13_inj[THEN iffD1]}) 1›)
      apply assumption
     apply assumption
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (rule conjI)
     apply (rule impI)
     apply (drule trans[OF sym])
      apply (rule trans[OF rv1_Cons])
      apply (rule trans[OF arg_cong[OF sum.case(2)]])
      apply (erule arg_cong[OF frombd_F13_tobd_F13])
     apply (erule allE)+
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (erule mp)
     apply (erule sym)

    apply (rule impI)
    apply (drule trans[OF sym])
     apply (rule trans[OF rv1_Cons])
     apply (rule trans[OF arg_cong[OF sum.case(2)]])
     apply (erule arg_cong[OF frombd_F13_tobd_F13])
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (erule mp)
    apply (erule sym)

   apply (rule impI)
   apply (drule ssubst_mem[OF sym[OF append_Cons]])
   apply (drule subsetD[OF equalityD1[OF Lev1_Suc]])
   apply (erule UnE)
    apply (erule CollectE exE conjE)+
    apply (drule list.inject[THEN iffD1])
    apply (erule conjE)
    apply (erule notE[OF Inr_not_Inl])

   apply (erule CollectE exE conjE)+
   apply (drule list.inject[THEN iffD1])
   apply (erule conjE)
   apply (drule Inr_inject)
   apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F13_inj[THEN iffD1]}) 1›)
     apply assumption
    apply assumption
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule conjI)
    apply (rule impI)
    apply (drule trans[OF sym])
     apply (rule trans[OF rv1_Cons])
     apply (rule trans[OF arg_cong[OF sum.case(2)]])
     apply (erule arg_cong[OF frombd_F13_tobd_F13])
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule mp)
    apply (erule sym)

   apply (rule impI)
   apply (drule trans[OF sym])
    apply (rule trans[OF rv1_Cons])
    apply (rule trans[OF arg_cong[OF sum.case(2)]])
    apply (erule arg_cong[OF frombd_F13_tobd_F13])
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule mp)
   apply (erule sym)

(*1/2*)

  apply (rule impI)
  apply (drule subsetD[OF equalityD1[OF Lev2_Suc]])
  apply (erule UnE)
   apply (erule CollectE exE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule conjI)
    apply (rule impI)
    apply (drule ssubst_mem[OF sym[OF append_Cons]])
    apply (drule subsetD[OF equalityD1[OF Lev2_Suc]])
    apply (erule UnE)
     apply (erule CollectE exE conjE)+
     apply (drule list.inject[THEN iffD1])
     apply (erule conjE)
     apply (drule Inl_inject)
     apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F22_inj[THEN iffD1]}) 1›)
       apply assumption
      apply assumption
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (rule conjI)
      apply (rule impI)
      apply (drule trans[OF sym])
       apply (rule trans[OF rv2_Cons])
       apply (rule trans[OF arg_cong[OF sum.case(1)]])
       apply (erule arg_cong[OF frombd_F22_tobd_F22])
      apply (erule allE)+
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (drule mp)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (drule mp)
       apply assumption
      apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
      apply (erule mp)
      apply (erule sym)

     apply (rule impI)
     apply (drule trans[OF sym])
      apply (rule trans[OF rv2_Cons])
      apply (rule trans[OF arg_cong[OF sum.case(1)]])
      apply (erule arg_cong[OF frombd_F22_tobd_F22])
     apply (erule allE)+
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (erule mp)
     apply (erule sym)

    apply (erule CollectE exE conjE)+
    apply (drule list.inject[THEN iffD1])
    apply (erule conjE)
    apply (erule notE[OF Inl_not_Inr])

   apply (rule impI)
   apply (drule ssubst_mem[OF sym[OF append_Cons]])
   apply (drule subsetD[OF equalityD1[OF Lev2_Suc]])
   apply (erule UnE)
    apply (erule CollectE exE conjE)+
    apply (drule list.inject[THEN iffD1])
    apply (erule conjE)
    apply (drule Inl_inject)
    apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F22_inj[THEN iffD1]}) 1›)
      apply assumption
     apply assumption
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (rule conjI)
     apply (rule impI)
     apply (drule trans[OF sym])
      apply (rule trans[OF rv2_Cons])
      apply (rule trans[OF arg_cong[OF sum.case(1)]])
      apply (erule arg_cong[OF frombd_F22_tobd_F22])
     apply (erule allE)+
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
     apply (drule mp)
      apply assumption
     apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (erule mp)
     apply (erule sym)

    apply (rule impI)
    apply (drule trans[OF sym])
     apply (rule trans[OF rv2_Cons])
     apply (rule trans[OF arg_cong[OF sum.case(1)]])
     apply (erule arg_cong[OF frombd_F22_tobd_F22])
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (erule mp)
    apply (erule sym)

   apply (erule CollectE exE conjE)+
   apply (drule list.inject[THEN iffD1])
   apply (erule conjE)
   apply (erule notE[OF Inl_not_Inr])
    (*outer UN1/2*)
  apply (erule CollectE exE conjE)+
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (rule conjI)
   apply (rule impI)
   apply (drule ssubst_mem[OF sym[OF append_Cons]])
   apply (drule subsetD[OF equalityD1[OF Lev2_Suc]])
   apply (erule UnE)
    apply (erule CollectE exE conjE)+
    apply (drule list.inject[THEN iffD1])
    apply (erule conjE)
    apply (erule notE[OF Inr_not_Inl])

   apply (erule CollectE exE conjE)+
   apply (drule list.inject[THEN iffD1])
   apply (erule conjE)
   apply (drule Inr_inject)
   apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F23_inj[THEN iffD1]}) 1›)
     apply assumption
    apply assumption
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule conjI)
    apply (rule impI)
    apply (drule trans[OF sym])
     apply (rule trans[OF rv2_Cons])
     apply (rule trans[OF arg_cong[OF sum.case(2)]])
     apply (erule arg_cong[OF frombd_F23_tobd_F23])
    apply (erule allE)+
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (drule mp)
     apply assumption
    apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (erule mp)
    apply (erule sym)

   apply (rule impI)
   apply (drule trans[OF sym])
    apply (rule trans[OF rv2_Cons])
    apply (rule trans[OF arg_cong[OF sum.case(2)]])
    apply (erule arg_cong[OF frombd_F23_tobd_F23])
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (erule mp)
   apply (erule sym)

  apply (rule impI)
  apply (drule ssubst_mem[OF sym[OF append_Cons]])
  apply (drule subsetD[OF equalityD1[OF Lev2_Suc]])
  apply (erule UnE)
   apply (erule CollectE exE conjE)+
   apply (drule list.inject[THEN iffD1])
   apply (erule conjE)
   apply (erule notE[OF Inr_not_Inl])

  apply (erule CollectE exE conjE)+
  apply (drule list.inject[THEN iffD1])
  apply (erule conjE)
  apply (drule Inr_inject)
  apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F23_inj[THEN iffD1]}) 1›)
    apply assumption
   apply assumption
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (rule conjI)
   apply (rule impI)
   apply (drule trans[OF sym])
    apply (rule trans[OF rv2_Cons])
    apply (rule trans[OF arg_cong[OF sum.case(2)]])
    apply (erule arg_cong[OF frombd_F23_tobd_F23])
   apply (erule allE)+
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (drule mp)
    apply assumption
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (erule mp)
   apply (erule sym)

  apply (rule impI)
  apply (drule trans[OF sym])
   apply (rule trans[OF rv2_Cons])
   apply (rule trans[OF arg_cong[OF sum.case(2)]])
   apply (erule arg_cong[OF frombd_F23_tobd_F23])
  apply (erule allE)+
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (drule mp)
   apply assumption
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (drule mp)
   apply assumption
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (erule mp)
  apply (erule sym)
  done

lemmas Fset_image_Lev' =
  spec[OF spec[OF spec[OF  spec[OF spec[OF spec[OF Fset_image_Lev]]]]]]
lemmas F1set2_image_Lev1 =
  mp[OF conjunct1[OF mp[OF conjunct1[OF mp[OF conjunct1[OF Fset_image_Lev']]]]]]
lemmas F1set2_image_Lev2 =
  mp[OF conjunct1[OF mp[OF conjunct1[OF mp[OF conjunct2[OF Fset_image_Lev']]]]]]
lemmas F1set3_image_Lev1 =
  mp[OF conjunct1[OF mp[OF conjunct2[OF mp[OF conjunct1[OF Fset_image_Lev']]]]]]
lemmas F1set3_image_Lev2 =
  mp[OF conjunct1[OF mp[OF conjunct2[OF mp[OF conjunct2[OF Fset_image_Lev']]]]]]
lemmas F2set2_image_Lev1 =
  mp[OF conjunct2[OF mp[OF conjunct1[OF mp[OF conjunct1[OF Fset_image_Lev']]]]]]
lemmas F2set2_image_Lev2 =
  mp[OF conjunct2[OF mp[OF conjunct1[OF mp[OF conjunct2[OF Fset_image_Lev']]]]]]
lemmas F2set3_image_Lev1 =
  mp[OF conjunct2[OF mp[OF conjunct2[OF mp[OF conjunct1[OF Fset_image_Lev']]]]]]
lemmas F2set3_image_Lev2 =
  mp[OF conjunct2[OF mp[OF conjunct2[OF mp[OF conjunct2[OF Fset_image_Lev']]]]]]

lemma mor_beh:
  "mor UNIV UNIV s1 s2 carT1 carT2 strT1 strT2 (beh1 s1 s2) (beh2 s1 s2)"
  apply (rule mor_cong)
    apply (rule ext[OF beh1_def])
   apply (rule ext[OF beh2_def])
  apply (tactic ‹rtac @{context} (@{thm mor_def} RS iffD2) 1›)
  apply (rule conjI)
   apply (rule conjI)
    apply (rule ballI)
    apply (rule subsetD[OF equalityD2[OF carT1_def]])
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (rule conjI)
     apply (rule conjI)
      apply (rule UN_I)
       apply (rule UNIV_I)
      apply (rule subsetD)
       apply (rule equalityD2)
       apply (rule Lev1_0)
      apply (rule singletonI)

     apply (rule ballI)
     apply (erule UN_E)
     apply (rule conjI)
      apply (rule ballI)
      apply (erule CollectE SuccD[elim_format] UN_E)+
      apply (rule rev_mp[OF rv1_Inl_last impI])
      apply (erule exE)
      apply (rule iffD2[OF isNode1_def])
      apply (rule exI)
      apply (rule conjI)
       apply (erule trans[OF sum.case_cong_weak])
       apply (rule sum.case(1))

      apply (rule conjI)
       apply (rule trans[OF F1.set_map(2)])
       apply (rule equalityI)
        apply (rule image_subsetI)
        apply (rule CollectI)
        apply (rule SuccI)
        apply (rule UN_I[OF UNIV_I])
        apply (erule F1set2_Lev1)
         apply assumption
        apply assumption
       apply (rule subsetI)
       apply (erule CollectE SuccD[elim_format] UN_E)+
       apply (erule thin_rl)
       apply (erule thin_rl)
       apply (erule thin_rl)
       apply (erule thin_rl)
       apply (rule F1set2_image_Lev1)
         apply assumption
        apply (drule length_Lev1)
        apply (tactic ‹hyp_subst_tac @{context} 1›)
        apply (drule length_Lev1')
        apply (erule subsetD[OF equalityD1[OF arg_cong[OF length_append_singleton]]])
       apply assumption

      apply (rule trans[OF F1.set_map(3)])
      apply (rule equalityI)
       apply (rule image_subsetI)
       apply (rule CollectI)
       apply (rule SuccI)
       apply (rule UN_I[OF UNIV_I])
       apply (erule F1set3_Lev1)
        apply assumption
       apply assumption
      apply (rule subsetI)
      apply (erule CollectE SuccD[elim_format] UN_E)+
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (rule F1set3_image_Lev1)
        apply assumption
       apply (drule length_Lev1)
       apply (tactic ‹hyp_subst_tac @{context} 1›)
       apply (drule length_Lev1')
       apply (erule subsetD[OF equalityD1[OF arg_cong[OF length_append_singleton]]])
      apply assumption

     apply (rule ballI)
     apply (erule CollectE SuccD[elim_format] UN_E)+
     apply (rule rev_mp[OF rv1_Inr_last impI])
     apply (erule exE)
     apply (rule iffD2[OF isNode2_def])
     apply (rule exI)
     apply (rule conjI)
      apply (erule trans[OF sum.case_cong_weak])
      apply (rule sum.case(2))

     apply (rule conjI)
      apply (rule trans[OF F2.set_map(2)])
      apply (rule equalityI)
       apply (rule image_subsetI)
       apply (rule CollectI)
       apply (rule SuccI)
       apply (rule UN_I[OF UNIV_I])
       apply (erule F2set2_Lev1)
        apply assumption
       apply assumption
      apply (rule subsetI)
      apply (erule CollectE SuccD[elim_format] UN_E)+
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (rule F2set2_image_Lev1)
        apply assumption
       apply (drule length_Lev1)
       apply (tactic ‹hyp_subst_tac @{context} 1›)
       apply (drule length_Lev1')
       apply (erule subsetD[OF equalityD1[OF arg_cong[OF length_append_singleton]]])
      apply assumption

     apply (rule trans[OF F2.set_map(3)])
     apply (rule equalityI)
      apply (rule image_subsetI)
      apply (rule CollectI)
      apply (rule SuccI)
      apply (rule UN_I[OF UNIV_I])
      apply (erule F2set3_Lev1)
       apply assumption
      apply assumption
     apply (rule subsetI)
     apply (erule CollectE SuccD[elim_format] UN_E)+
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (rule F2set3_image_Lev1)
       apply assumption
      apply (drule length_Lev1)
      apply (tactic ‹hyp_subst_tac @{context} 1›)
      apply (drule length_Lev1')
      apply (erule subsetD[OF equalityD1[OF arg_cong[OF length_append_singleton]]])
     apply assumption

    apply (rule iffD2[OF isNode1_def])
    apply (rule exI)
    apply (rule conjI)
     apply (rule trans[OF sum.case_cong_weak])
      apply (rule rv1_Nil)
     apply (rule sum.case(1))

    apply (rule conjI)
     apply (rule trans[OF F1.set_map(2)])
     apply (rule equalityI)
      apply (rule image_subsetI)
      apply (rule CollectI)
      apply (rule SuccI)
      apply (rule UN_I[OF UNIV_I])
      apply (rule F1set2_Lev1)
        apply (rule subsetD[OF equalityD2])
         apply (rule Lev1_0)
        apply (rule singletonI)
       apply (rule rv1_Nil)
      apply assumption
     apply (rule subsetI)
     apply (erule CollectE SuccD[elim_format] UN_E)+
     apply (rule F1set2_image_Lev1)
       apply (rule subsetD[OF equalityD2[OF Lev1_0]])
       apply (rule singletonI)
      apply (drule length_Lev1')
      apply (erule subsetD[OF equalityD1[OF arg_cong[OF
            trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]])
     apply (rule rv1_Nil)

    apply (rule trans[OF F1.set_map(3)])
    apply (rule equalityI)
     apply (rule image_subsetI)
     apply (rule CollectI)
     apply (rule SuccI)
     apply (rule UN_I[OF UNIV_I])
     apply (rule F1set3_Lev1)
       apply (rule subsetD[OF equalityD2])
        apply (rule Lev1_0)
       apply (rule singletonI)
      apply (rule rv1_Nil)
     apply assumption
    apply (rule subsetI)
    apply (erule CollectE SuccD[elim_format] UN_E)+
    apply (rule F1set3_image_Lev1)
      apply (rule subsetD[OF equalityD2[OF Lev1_0]])
      apply (rule singletonI)
     apply (drule length_Lev1')
     apply (erule subsetD[OF equalityD1[OF arg_cong[OF
            trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]])
    apply (rule rv1_Nil)

(**)

   apply (rule ballI)
   apply (rule subsetD[OF equalityD2[OF carT2_def]])
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (rule conjI)
    apply (rule conjI)
     apply (rule UN_I)
      apply (rule UNIV_I)
     apply (rule subsetD)
      apply (rule equalityD2)
      apply (rule Lev2_0)
     apply (rule singletonI)

    apply (rule ballI)
    apply (erule UN_E)
    apply (rule conjI)
     apply (rule ballI)
     apply (erule CollectE SuccD[elim_format] UN_E)+
     apply (rule rev_mp[OF rv2_Inl_last impI])
     apply (erule exE)
     apply (rule iffD2[OF isNode1_def])
     apply (rule exI)
     apply (rule conjI)
      apply (erule trans[OF sum.case_cong_weak])
      apply (rule sum.case(1))

     apply (rule conjI)
      apply (rule trans[OF F1.set_map(2)])
      apply (rule equalityI)
       apply (rule image_subsetI)
       apply (rule CollectI)
       apply (rule SuccI)
       apply (rule UN_I[OF UNIV_I])
       apply (erule F1set2_Lev2)
        apply assumption
       apply assumption
      apply (rule subsetI)
      apply (erule CollectE SuccD[elim_format] UN_E)+
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (erule thin_rl)
      apply (rule F1set2_image_Lev2)
        apply assumption
       apply (drule length_Lev2)
       apply (tactic ‹hyp_subst_tac @{context} 1›)
       apply (drule length_Lev2')
       apply (erule subsetD[OF equalityD1[OF arg_cong[OF length_append_singleton]]])
      apply assumption

     apply (rule trans[OF F1.set_map(3)])
     apply (rule equalityI)
      apply (rule image_subsetI)
      apply (rule CollectI)
      apply (rule SuccI)
      apply (rule UN_I[OF UNIV_I])
      apply (erule F1set3_Lev2)
       apply assumption
      apply assumption
     apply (rule subsetI)
     apply (erule CollectE SuccD[elim_format] UN_E)+
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (rule F1set3_image_Lev2)
       apply assumption
      apply (drule length_Lev2)
      apply (tactic ‹hyp_subst_tac @{context} 1›)
      apply (drule length_Lev2')
      apply (erule subsetD[OF equalityD1[OF arg_cong[OF length_append_singleton]]])
     apply assumption

    apply (rule ballI)
    apply (erule CollectE SuccD[elim_format] UN_E)+
    apply (rule rev_mp[OF rv2_Inr_last impI])
    apply (erule exE)
    apply (rule iffD2[OF isNode2_def])
    apply (rule exI)
    apply (rule conjI)
     apply (erule trans[OF sum.case_cong_weak])
     apply (rule sum.case(2))

    apply (rule conjI)
     apply (rule trans[OF F2.set_map(2)])
     apply (rule equalityI)
      apply (rule image_subsetI)
      apply (rule CollectI)
      apply (rule SuccI)
      apply (rule UN_I[OF UNIV_I])
      apply (erule F2set2_Lev2)
       apply assumption
      apply assumption
     apply (rule subsetI)
     apply (erule CollectE SuccD[elim_format] UN_E)+
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply (rule F2set2_image_Lev2)
       apply assumption
      apply (drule length_Lev2)
      apply (tactic ‹hyp_subst_tac @{context} 1›)
      apply (drule length_Lev2')
      apply (erule subsetD[OF equalityD1[OF arg_cong[OF length_append_singleton]]])
     apply assumption

    apply (rule trans[OF F2.set_map(3)])
    apply (rule equalityI)
     apply (rule image_subsetI)
     apply (rule CollectI)
     apply (rule SuccI)
     apply (rule UN_I[OF UNIV_I])
     apply (erule F2set3_Lev2)
      apply assumption
     apply assumption
    apply (rule subsetI)
    apply (erule CollectE SuccD[elim_format] UN_E)+
    apply (erule thin_rl)
    apply (erule thin_rl)
    apply (erule thin_rl)
    apply (erule thin_rl)
    apply (rule F2set3_image_Lev2)
      apply assumption
     apply (drule length_Lev2)
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (drule length_Lev2')
     apply (erule subsetD[OF equalityD1[OF arg_cong[OF length_append_singleton]]])
    apply assumption

   apply (rule iffD2[OF isNode2_def])
   apply (rule exI)
   apply (rule conjI)
    apply (rule trans[OF sum.case_cong_weak])
     apply (rule rv2_Nil)
    apply (rule sum.case(2))

   apply (rule conjI)
    apply (rule trans[OF F2.set_map(2)])
    apply (rule equalityI)
     apply (rule image_subsetI)
     apply (rule CollectI)
     apply (rule SuccI)
     apply (rule UN_I[OF UNIV_I])
     apply (rule F2set2_Lev2)
       apply (rule subsetD[OF equalityD2[OF Lev2_0]])
       apply (rule singletonI)
      apply (rule rv2_Nil)
     apply assumption
    apply (rule subsetI)
    apply (erule CollectE SuccD[elim_format] UN_E)+
    apply (rule F2set2_image_Lev2)
      apply (rule subsetD[OF equalityD2[OF Lev2_0]])
      apply (rule singletonI)
     apply (drule length_Lev2')
     apply (erule subsetD[OF equalityD1[OF arg_cong[OF
            trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]])
    apply (rule rv2_Nil)

   apply (rule trans[OF F2.set_map(3)])
   apply (rule equalityI)
    apply (rule image_subsetI)
    apply (rule CollectI)
    apply (rule SuccI)
    apply (rule UN_I[OF UNIV_I])
    apply (rule F2set3_Lev2)
      apply (rule subsetD[OF equalityD2])
       apply (rule Lev2_0)
      apply (rule singletonI)
     apply (rule rv2_Nil)
    apply assumption
   apply (rule subsetI)
   apply (erule CollectE SuccD[elim_format] UN_E)+
   apply (rule F2set3_image_Lev2)
     apply (rule subsetD[OF equalityD2[OF Lev2_0]])
     apply (rule singletonI)
    apply (drule length_Lev2')
    apply (erule subsetD[OF equalityD1[OF arg_cong[OF
            trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]])
   apply (rule rv2_Nil)

(*mor_tac*)

  apply (rule conjI)
   apply (rule ballI)
   apply (rule sym)
   apply (rule trans)
    apply (rule trans[OF fun_cong[OF strT1_def] prod.case])
   apply (tactic ‹CONVERSION (Conv.top_conv
 (K (Conv.try_conv (Conv.rewr_conv (@{thm rv1_Nil} RS eq_reflection)))) @{context}) 1›)
   apply (rule trans[OF sum.case_cong_weak])
    apply (rule sum.case(1))
   apply (rule trans[OF sum.case(1)])
   apply (rule trans[OF F1map_comp_id])
   apply (rule F1.map_cong0[OF refl])
    apply (rule trans)
     apply (rule o_apply)
    apply (rule iffD2)
     apply (rule prod.inject)
    apply (rule conjI)
     apply (rule trans)
      apply (rule Shift_def)

(*UN_Lev*)
     apply (rule equalityI)
      apply (rule subsetI)
      apply (erule thin_rl)
      apply (erule CollectE UN_E)+
      apply (drule length_Lev1')
      apply (drule asm_rl)
      apply (erule thin_rl)
      apply (drule rev_subsetD[OF _ equalityD1])
       apply (rule trans[OF arg_cong[OF length_Cons]])
       apply (rule Lev1_Suc)
      apply (erule UnE)
       apply (erule CollectE exE conjE)+
       apply (tactic ‹dtac @{context} @{thm list.inject[THEN iffD1]} 1›)
       apply (erule conjE)
       apply (drule Inl_inject)
       apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F12_inj[THEN iffD1]}) 1›)
         apply assumption
        apply assumption
       apply (tactic ‹hyp_subst_tac @{context} 1›)
       apply (erule UN_I[OF UNIV_I])
      apply (erule CollectE exE conjE)+
      apply (tactic ‹dtac @{context} @{thm list.inject[THEN iffD1]} 1›)
      apply (erule conjE)
      apply (erule notE[OF Inl_not_Inr])

     apply (rule UN_least)
     apply (rule subsetI)
     apply (rule CollectI)
     apply (rule UN_I[OF UNIV_I])
     apply (rule subsetD[OF equalityD2])
      apply (rule Lev1_Suc)
     apply (rule UnI1)
     apply (rule CollectI)
     apply (rule exI)+
     apply (rule conjI)
      apply (rule refl)
     apply (erule conjI)
     apply assumption
    (**)

    apply (rule trans)
     apply (rule shift_def)
    apply (rule iffD2)
     apply (rule fun_eq_iff)
    apply (rule allI)
    apply (tactic ‹CONVERSION (Conv.top_conv
 (K (Conv.try_conv (Conv.rewr_conv (@{thm rv1_Cons} RS eq_reflection)))) @{context}) 1›)
    apply (rule sum.case_cong_weak)
    apply (rule trans[OF sum.case(1)])
    apply (drule frombd_F12_tobd_F12)
    apply (erule arg_cong)

   apply (rule trans)
    apply (rule o_apply)
   apply (rule iffD2)
    apply (rule prod.inject)
   apply (rule conjI)
    apply (rule trans)
     apply (rule Shift_def)

(*UN_Lev*)
    apply (rule equalityI)
     apply (rule subsetI)
     apply (erule thin_rl)
     apply (erule CollectE UN_E)+
     apply (drule length_Lev1')
     apply (drule asm_rl)
     apply (erule thin_rl)
     apply (drule rev_subsetD[OF _ equalityD1])
      apply (rule trans[OF arg_cong[OF length_Cons]])
      apply (rule Lev1_Suc)
     apply (erule UnE)
      apply (erule CollectE exE conjE)+
      apply (tactic ‹dtac @{context} @{thm list.inject[THEN iffD1]} 1›)
      apply (erule conjE)
      apply (erule notE[OF Inr_not_Inl])
     apply (erule CollectE exE conjE)+
     apply (tactic ‹dtac @{context} @{thm list.inject[THEN iffD1]} 1›)
     apply (erule conjE)
     apply (drule Inr_inject)
     apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F13_inj[THEN iffD1]}) 1›)
       apply assumption
      apply assumption
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (erule UN_I[OF UNIV_I])

    apply (rule UN_least)
    apply (rule subsetI)
    apply (rule CollectI)
    apply (rule UN_I[OF UNIV_I])
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev1_Suc)
    apply (rule UnI2)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (erule conjI)
    apply assumption
    (**)

   apply (rule trans)
    apply (rule shift_def)
   apply (rule iffD2)
    apply (rule fun_eq_iff)
   apply (rule allI)
   apply (rule sum.case_cong_weak)
   apply (rule trans[OF rv1_Cons])
   apply (rule trans[OF sum.case(2)])
   apply (erule arg_cong[OF frombd_F13_tobd_F13])

(**)

  apply (rule ballI)
  apply (rule sym)
  apply (rule trans)
   apply (rule trans[OF fun_cong[OF strT2_def] prod.case])
  apply (rule trans[OF sum.case_cong_weak[OF trans[OF sum.case_cong_weak]]])
    apply (rule rv2_Nil)
   apply (rule sum.case(2))
  apply (rule trans[OF sum.case(2)])
  apply (rule trans[OF F2map_comp_id])
  apply (rule F2.map_cong0[OF refl])
   apply (rule trans)
    apply (rule o_apply)
   apply (rule iffD2)
    apply (rule prod.inject)
   apply (rule conjI)
    apply (rule trans)
     apply (rule Shift_def)

(*UN_Lev*)
    apply (rule equalityI)
     apply (rule subsetI)
     apply (erule thin_rl)
     apply (erule CollectE UN_E)+
     apply (drule length_Lev2')
     apply (drule asm_rl)
     apply (erule thin_rl)
     apply (drule rev_subsetD[OF _ equalityD1])
      apply (rule trans[OF arg_cong[OF length_Cons]])
      apply (rule Lev2_Suc)
     apply (erule UnE)
      apply (erule CollectE exE conjE)+
      apply (tactic ‹dtac @{context} @{thm list.inject[THEN iffD1]} 1›)
      apply (erule conjE)
      apply (drule Inl_inject)
      apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F22_inj[THEN iffD1]}) 1›)
        apply assumption
       apply assumption
      apply (tactic ‹hyp_subst_tac @{context} 1›)
      apply (erule UN_I[OF UNIV_I])
     apply (erule CollectE exE conjE)+
     apply (tactic ‹dtac @{context} @{thm list.inject[THEN iffD1]} 1›)
     apply (erule conjE)
     apply (erule notE[OF Inl_not_Inr])

    apply (rule UN_least)
    apply (rule subsetI)
    apply (rule CollectI)
    apply (rule UN_I[OF UNIV_I])
    apply (rule subsetD[OF equalityD2])
     apply (rule Lev2_Suc)
    apply (rule UnI1)
    apply (rule CollectI)
    apply (rule exI)+
    apply (rule conjI)
     apply (rule refl)
    apply (erule conjI)
    apply assumption
    (**)

   apply (rule trans)
    apply (rule shift_def)
   apply (rule iffD2)
    apply (rule fun_eq_iff)
   apply (rule allI)
   apply (rule sum.case_cong_weak)
   apply (rule trans[OF rv2_Cons])
   apply (rule trans[OF arg_cong[OF sum.case(1)]])
   apply (erule arg_cong[OF frombd_F22_tobd_F22])

  apply (rule trans)
   apply (rule o_apply)
  apply (rule iffD2)
   apply (rule prod.inject)
  apply (rule conjI)
   apply (rule trans)
    apply (rule Shift_def)

(*UN_Lev*)
   apply (rule equalityI)
    apply (rule subsetI)
    apply (erule thin_rl)
    apply (erule CollectE UN_E)+
    apply (drule length_Lev2')
    apply (drule asm_rl)
    apply (erule thin_rl)
    apply (drule rev_subsetD[OF _ equalityD1])
     apply (rule trans[OF arg_cong[OF length_Cons]])
     apply (rule Lev2_Suc)
    apply (erule UnE)
     apply (erule CollectE exE conjE)+
     apply (tactic ‹dtac @{context} @{thm list.inject[THEN iffD1]} 1›)
     apply (erule conjE)
     apply (erule notE[OF Inr_not_Inl])
    apply (erule CollectE exE conjE)+
    apply (tactic ‹dtac @{context} @{thm list.inject[THEN iffD1]} 1›)
    apply (erule conjE)
    apply (drule Inr_inject)
    apply (tactic ‹dtac @{context}
 (Thm.permute_prems 0 2 @{thm tobd_F23_inj[THEN iffD1]}) 1›)
      apply assumption
     apply assumption
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (erule UN_I[OF UNIV_I])

   apply (rule UN_least)
   apply (rule subsetI)
   apply (rule CollectI)
   apply (rule UN_I[OF UNIV_I])
   apply (rule subsetD[OF equalityD2])
    apply (rule Lev2_Suc)
   apply (rule UnI2)
   apply (rule CollectI)
   apply (rule exI)+
   apply (rule conjI)
    apply (rule refl)
   apply (erule conjI)
   apply assumption
    (**)

  apply (rule trans)
   apply (rule shift_def)
  apply (rule iffD2)
   apply (rule fun_eq_iff)
  apply (rule allI)

  apply (rule sum.case_cong_weak)
  apply (rule trans[OF rv2_Cons])
  apply (rule trans[OF arg_cong[OF sum.case(2)]])
  apply (erule arg_cong[OF frombd_F23_tobd_F23])
  done

subsection ‹Quotient Coalgebra›

(* final coalgebra *)
abbreviation car_final1 where
  "car_final1 ≡ carT1 // (lsbis1 carT1 carT2 strT1 strT2)"
abbreviation car_final2 where
  "car_final2 ≡ carT2 // (lsbis2 carT1 carT2 strT1 strT2)"
abbreviation str_final1 where
  "str_final1 ≡ univ (F1map id
    (Equiv_Relations.proj (lsbis1 carT1 carT2 strT1 strT2))
    (Equiv_Relations.proj (lsbis2 carT1 carT2 strT1 strT2)) o strT1)"
abbreviation str_final2 where
  "str_final2 ≡ univ (F2map id
    (Equiv_Relations.proj (lsbis1 carT1 carT2 strT1 strT2))
    (Equiv_Relations.proj (lsbis2 carT1 carT2 strT1 strT2)) o strT2)"

lemma congruent_strQ1: "congruent (lsbis1 carT1 carT2 strT1 strT2 :: 'a carrier rel)
  (F1map id (Equiv_Relations.proj (lsbis1 carT1 carT2 strT1 strT2 :: 'a carrier rel))
            (Equiv_Relations.proj (lsbis2 carT1 carT2 strT1 strT2 :: 'a carrier rel)) o strT1)"
  apply (rule congruentI)
  apply (drule lsbisE1)
  apply (erule bexE conjE CollectE)+
  apply (rule trans[OF o_apply])
  apply (erule trans[OF arg_cong[OF sym]])
  apply (rule trans[OF F1map_comp_id])
  apply (rule trans[OF F1.map_cong0])
     apply (rule refl)
    apply (rule equiv_proj)
     apply (rule equiv_lsbis1)
     apply (rule coalg_T)
    apply (erule subsetD)
    apply assumption
   apply (rule equiv_proj)
    apply (rule equiv_lsbis2)
    apply (rule coalg_T)
   apply (erule subsetD)
   apply assumption
  apply (rule sym)
  apply (rule trans[OF o_apply])
  apply (erule trans[OF arg_cong[OF sym]])
  apply (rule F1map_comp_id)
  done

lemma congruent_strQ2: "congruent (lsbis2 carT1 carT2 strT1 strT2 :: 'a carrier rel)
  (F2map id (Equiv_Relations.proj (lsbis1 carT1 carT2 strT1 strT2 :: 'a carrier rel))
            (Equiv_Relations.proj (lsbis2 carT1 carT2 strT1 strT2 :: 'a carrier rel)) o strT2)"
  apply (rule congruentI)
  apply (drule lsbisE2)
  apply (erule bexE conjE CollectE)+
  apply (rule trans[OF o_apply])
  apply (erule trans[OF arg_cong[OF sym]])
  apply (rule trans[OF F2map_comp_id])
  apply (rule trans[OF F2.map_cong0])
     apply (rule refl)
    apply (rule equiv_proj)
     apply (rule equiv_lsbis1)
     apply (rule coalg_T)
    apply (erule subsetD)
    apply assumption
   apply (rule equiv_proj)
    apply (rule equiv_lsbis2)
    apply (rule coalg_T)
   apply (erule subsetD)
   apply assumption
  apply (rule sym)
  apply (rule trans[OF o_apply])
  apply (erule trans[OF arg_cong[OF sym]])
  apply (rule F2map_comp_id)
  done

lemma coalg_final:
  "coalg car_final1 car_final2 str_final1 str_final2"
  apply (tactic ‹rtac @{context} (@{thm coalg_def} RS iffD2) 1›)
  apply (rule conjI)
   apply (rule univ_preserves)
     apply (rule equiv_lsbis1)
     apply (rule coalg_T)
    apply (rule congruent_strQ1)
   apply (rule ballI)
   apply (rule ssubst_mem)
    apply (rule o_apply)
   apply (rule CollectI)
   apply (rule conjI)
    apply (rule subset_UNIV)
   apply (rule conjI)
    apply (rule ord_eq_le_trans[OF F1.set_map(2)])
    apply (rule image_subsetI)
    apply (rule iffD2)
     apply (rule proj_in_iff)
     apply (rule equiv_lsbis1[OF coalg_T])
    apply (erule rev_subsetD)
    apply (erule coalg_F1set2[OF coalg_T])
   apply (rule ord_eq_le_trans[OF F1.set_map(3)])
   apply (rule image_subsetI)
   apply (rule iffD2)
    apply (rule proj_in_iff)
    apply (rule equiv_lsbis2[OF coalg_T])
   apply (erule rev_subsetD)
   apply (erule coalg_F1set3[OF coalg_T])

  apply (rule univ_preserves)
    apply (rule equiv_lsbis2)
    apply (rule coalg_T)
   apply (rule congruent_strQ2)
  apply (rule ballI)
  apply (tactic ‹stac @{context} @{thm o_apply} 1›)
  apply (rule CollectI)
  apply (rule conjI)
   apply (rule subset_UNIV)
  apply (rule conjI)
   apply (rule ord_eq_le_trans[OF F2.set_map(2)])
   apply (rule image_subsetI)
   apply (rule iffD2)
    apply (rule proj_in_iff)
    apply (rule equiv_lsbis1[OF coalg_T])
   apply (erule rev_subsetD)
   apply (erule coalg_F2set2[OF coalg_T])
  apply (rule ord_eq_le_trans[OF F2.set_map(3)])
  apply (rule image_subsetI)
  apply (rule iffD2)
   apply (rule proj_in_iff)
   apply (rule equiv_lsbis2[OF coalg_T])
  apply (erule rev_subsetD)
  apply (erule coalg_F2set3[OF coalg_T])
  done

lemma mor_T_final:
  "mor carT1 carT2 strT1 strT2 car_final1 car_final2 str_final1 str_final2
  (Equiv_Relations.proj (lsbis1 carT1 carT2 strT1 strT2))
  (Equiv_Relations.proj (lsbis2 carT1 carT2 strT1 strT2))"
  apply (tactic ‹rtac @{context} (@{thm mor_def} RS iffD2) 1›)
  apply (rule conjI)
   apply (rule conjI)
    apply (rule ballI)
    apply (rule iffD2)
     apply (rule proj_in_iff)
     apply (rule equiv_lsbis1[OF coalg_T])
    apply assumption
   apply (rule ballI)
   apply (rule iffD2)
    apply (rule proj_in_iff)
    apply (rule equiv_lsbis2[OF coalg_T])
   apply assumption

  apply (rule conjI)
   apply (rule ballI)
   apply (rule sym)
   apply (rule trans)
    apply (rule univ_commute)
      apply (rule equiv_lsbis1[OF coalg_T])
     apply (rule congruent_strQ1)
    apply assumption
   apply (rule o_apply)

  apply (rule ballI)
  apply (rule sym)
  apply (rule trans)
   apply (rule univ_commute)
     apply (rule equiv_lsbis2[OF coalg_T])
    apply (rule congruent_strQ2)
   apply assumption
  apply (rule o_apply)
  done

lemmas mor_final = mor_comp[OF mor_beh mor_T_final]
lemmas in_car_final1 = mor_image1'[OF mor_final UNIV_I]
lemmas in_car_final2 = mor_image2'[OF mor_final UNIV_I]


(* The final coalgebra as a type *)

typedef (overloaded) 'a JF1 = "car_final1 :: 'a carrier set set"
  by (rule exI) (rule in_car_final1)

typedef (overloaded) 'a JF2 = "car_final2 :: 'a carrier set set"
  by (rule exI) (rule in_car_final2)

(* unfold & unfold *)
definition dtor1 where
  "dtor1 x = F1map id Abs_JF1 Abs_JF2 (str_final1 (Rep_JF1 x))"
definition dtor2 where
  "dtor2 x = F2map id Abs_JF1 Abs_JF2 (str_final2 (Rep_JF2 x))"

lemma mor_Rep_JF: "mor UNIV UNIV dtor1 dtor2
  car_final1 car_final2 str_final1 str_final2
  Rep_JF1 Rep_JF2"
  unfolding mor_def dtor1_def dtor2_def
  apply (rule conjI)
   apply (rule conjI)
    apply (rule ballI)
    apply (rule Rep_JF1)
   apply (rule ballI)
   apply (rule Rep_JF2)

  apply (rule conjI)
   apply (rule ballI)
   apply (rule trans[OF F1map_comp_id])
   apply (rule F1map_congL)
    apply (rule ballI)
    apply (rule trans[OF o_apply])
    apply (rule Abs_JF1_inverse)
    apply (erule rev_subsetD)
    apply (rule coalg_F1set2)
     apply (rule coalg_final)
    apply (rule Rep_JF1)
   apply (rule ballI)
   apply (rule trans[OF o_apply])
   apply (rule Abs_JF2_inverse)
   apply (erule rev_subsetD)
   apply (rule coalg_F1set3)
    apply (rule coalg_final)
   apply (rule Rep_JF1)

  apply (rule ballI)
  apply (rule trans[OF F2map_comp_id])
  apply (rule F2map_congL)
   apply (rule ballI)
   apply (rule trans[OF o_apply])
   apply (rule Abs_JF1_inverse)
   apply (erule rev_subsetD)
   apply (rule coalg_F2set2)
    apply (rule coalg_final)
   apply (rule Rep_JF2)
  apply (rule ballI)
  apply (rule trans[OF o_apply])
  apply (rule Abs_JF2_inverse)
  apply (erule rev_subsetD)
  apply (rule coalg_F2set3)
   apply (rule coalg_final)
  apply (rule Rep_JF2)
  done

lemma mor_Abs_JF: "mor car_final1 car_final2 str_final1 str_final2
  UNIV UNIV dtor1 dtor2 Abs_JF1 Abs_JF2"
  unfolding mor_def dtor1_def dtor2_def
  apply (rule conjI)
   apply (rule conjI)
    apply (rule ballI)
    apply (rule UNIV_I)
   apply (rule ballI)
   apply (rule UNIV_I)

  apply (rule conjI)
   apply (rule ballI)
   apply (erule sym[OF arg_cong[OF Abs_JF1_inverse]])
  apply (rule ballI)
  apply (erule sym[OF arg_cong[OF Abs_JF2_inverse]])
  done

definition unfold1 where
  "unfold1 s1 s2 x =
     Abs_JF1 ((Equiv_Relations.proj (lsbis1 carT1 carT2 strT1 strT2) o beh1 s1 s2) x)"
definition unfold2 where
  "unfold2 s1 s2 x =
     Abs_JF2 ((Equiv_Relations.proj (lsbis2 carT1 carT2 strT1 strT2) o beh2 s1 s2) x)"

lemma mor_unfold:
  "mor UNIV UNIV s1 s2 UNIV UNIV dtor1 dtor2 (unfold1 s1 s2) (unfold2 s1 s2)"
  apply (rule iffD2)
   apply (rule mor_UNIV)
  apply (rule conjI)
   apply (rule ext)
   apply (rule sym[OF trans[OF o_apply]])
   apply (rule trans[OF dtor1_def])
   apply (rule trans[OF arg_cong[OF unfold1_def]])
   apply (rule trans[OF arg_cong[OF Abs_JF1_inverse[OF in_car_final1]]])
   apply (rule trans[OF arg_cong[OF sym[OF morE1[OF mor_final UNIV_I]]]])
   apply (rule trans[OF F1map_comp_id])
   apply (rule sym[OF trans[OF o_apply]])
   apply (rule F1.map_cong0)
     apply (rule refl)
    apply (rule trans[OF unfold1_def])
    apply (rule sym[OF o_apply])
   apply (rule trans[OF unfold2_def])
   apply (rule sym[OF o_apply])

  apply (rule ext)
  apply (rule sym[OF trans[OF o_apply]])
  apply (rule trans[OF dtor2_def])
  apply (rule trans[OF arg_cong[OF unfold2_def]])
  apply (rule trans[OF arg_cong[OF Abs_JF2_inverse[OF in_car_final2]]])
  apply (rule trans[OF arg_cong[OF sym[OF morE2[OF mor_final UNIV_I]]]])
  apply (rule trans[OF F2map_comp_id])
  apply (rule sym[OF trans[OF o_apply]])
  apply (rule F2.map_cong0)
    apply (rule refl)
   apply (rule trans[OF unfold1_def])
   apply (rule sym[OF o_apply])
  apply (rule trans[OF unfold2_def])
  apply (rule sym[OF o_apply])
  done

lemmas unfold1 = sym[OF morE1[OF mor_unfold UNIV_I]]
lemmas unfold2 = sym[OF morE2[OF mor_unfold UNIV_I]]

lemma JF_cind: "sbis UNIV UNIV dtor1 dtor2 R1 R2 ==> R1 ⊆ Id ∧ R2 ⊆ Id"
  apply (rule rev_mp)
   apply (tactic ‹forward_tac @{context} @{thms bis_def[THEN iffD1]} 1›)
   apply (erule conjE)+
   apply (rule bis_cong)
     apply (rule bis_Comp)
      apply (rule bis_converse)
      apply (rule bis_Gr)
       apply (rule tcoalg)
      apply (rule mor_Rep_JF)
     apply (rule bis_Comp)
      apply assumption
     apply (rule bis_Gr)
      apply (rule tcoalg)
     apply (rule mor_Rep_JF)
    apply (erule relImage_Gr)
   apply (erule relImage_Gr)

  apply (rule impI)
  apply (rule rev_mp)
   apply (rule bis_cong)
     apply (rule bis_Comp)
      apply (rule bis_Gr)
       apply (rule coalg_T)
      apply (rule mor_T_final)
     apply (rule bis_Comp)
      apply (rule sbis_lsbis)
     apply (rule bis_converse)
     apply (rule bis_Gr)
      apply (rule coalg_T)
     apply (rule mor_T_final)
    apply (rule relInvImage_Gr[OF lsbis1_incl])
   apply (rule relInvImage_Gr[OF lsbis2_incl])

  apply (rule impI)
  apply (rule conjI)
   apply (rule subset_trans)
    apply (rule relInvImage_UNIV_relImage)
   apply (rule subset_trans)
    apply (rule relInvImage_mono)
    apply (rule subset_trans)
     apply (erule incl_lsbis1)
    apply (rule ord_eq_le_trans)
     apply (rule sym[OF relImage_relInvImage])
     apply (rule xt1(3))
      apply (rule Sigma_cong)
       apply (rule proj_image)
      apply (rule proj_image)
     apply (rule lsbis1_incl)
    apply (rule subset_trans)
     apply (rule relImage_mono)
     apply (rule incl_lsbis1)
     apply assumption
    apply (rule relImage_proj)
    apply (rule equiv_lsbis1[OF coalg_T])
   apply (rule relInvImage_Id_on)
   apply (rule Rep_JF1_inject)

  apply (rule subset_trans)
   apply (rule relInvImage_UNIV_relImage)
  apply (rule subset_trans)
   apply (rule relInvImage_mono)
   apply (rule subset_trans)
    apply (erule incl_lsbis2)
   apply (rule ord_eq_le_trans)
    apply (rule sym[OF relImage_relInvImage])
    apply (rule xt1(3))
     apply (rule Sigma_cong)
      apply (rule proj_image)
     apply (rule proj_image)
    apply (rule lsbis2_incl)
   apply (rule subset_trans)
    apply (rule relImage_mono)
    apply (rule incl_lsbis2)
    apply assumption
   apply (rule relImage_proj)
   apply (rule equiv_lsbis2[OF coalg_T])
  apply (rule relInvImage_Id_on)
  apply (rule Rep_JF2_inject)
  done

lemmas JF_cind1 = conjunct1[OF JF_cind]
lemmas JF_cind2 = conjunct2[OF JF_cind]

lemma unfold_unique_mor:
  "mor UNIV UNIV s1 s2 UNIV UNIV dtor1 dtor2 f1 f2 ==>
   f1 = unfold1 s1 s2 ∧ f2 = unfold2 s1 s2"
  apply (rule conjI)
   apply (rule ext)
   apply (erule IdD[OF subsetD[OF JF_cind1[OF bis_image2[OF tcoalg _ tcoalg]]]])
    apply (rule mor_comp[OF mor_final mor_Abs_JF])
   apply (rule image2_eqI)
     apply (rule refl)
    apply (rule trans[OF arg_cong[OF unfold1_def]])
    apply (rule sym[OF o_apply])
   apply (rule UNIV_I)

  apply (rule ext)
  apply (erule IdD[OF subsetD[OF JF_cind2[OF bis_image2[OF tcoalg _ tcoalg]]]])
   apply (rule mor_comp[OF mor_final mor_Abs_JF])
  apply (rule image2_eqI)
    apply (rule refl)
   apply (rule trans[OF arg_cong[OF unfold2_def]])
   apply (rule sym[OF o_apply])
  apply (rule UNIV_I)
  done

lemmas unfold_unique = unfold_unique_mor[OF iffD2[OF mor_UNIV], OF conjI]
lemmas unfold1_dtor = sym[OF conjunct1[OF unfold_unique_mor[OF mor_id]]]
lemmas unfold2_dtor = sym[OF conjunct2[OF unfold_unique_mor[OF mor_id]]]

lemmas unfold1_o_dtor1 =
  trans[OF conjunct1[OF unfold_unique_mor[OF mor_comp[OF mor_str mor_unfold]]] unfold1_dtor]
lemmas unfold2_o_dtor2 =
  trans[OF conjunct2[OF unfold_unique_mor[OF mor_comp[OF mor_str mor_unfold]]] unfold2_dtor]

(* the fold operator *)
definition ctor1 where "ctor1 = unfold1 (F1map id dtor1 dtor2) (F2map id dtor1 dtor2)"
definition ctor2 where "ctor2 = unfold2 (F1map id dtor1 dtor2) (F2map id dtor1 dtor2)"

lemma ctor1_o_dtor1:
  "ctor1 o dtor1 = id"
  unfolding ctor1_def
  apply (rule unfold1_o_dtor1)
  done

lemma ctor2_o_dtor2:
  "ctor2 o dtor2 = id"
  unfolding ctor2_def
  apply (rule unfold2_o_dtor2)
  done

lemma dtor1_o_ctor1:
  "dtor1 o ctor1 = id"
  unfolding ctor1_def
  apply (rule ext)
  apply (rule trans[OF o_apply])
  apply (rule trans[OF unfold1])
  apply (rule trans[OF F1map_comp_id])
  apply (rule trans[OF F1map_congL])
    apply (rule ballI)
    apply (rule trans[OF fun_cong[OF unfold1_o_dtor1] id_apply])
   apply (rule ballI)
   apply (rule trans[OF fun_cong[OF unfold2_o_dtor2] id_apply])
  apply (rule sym[OF id_apply])
  done

lemma dtor2_o_ctor2:
  "dtor2 o ctor2 = id"
  unfolding ctor2_def
  apply (rule ext)
  apply (rule trans[OF o_apply])
  apply (rule trans[OF unfold2])
  apply (rule trans[OF F2map_comp_id])
  apply (rule trans[OF F2map_congL])
    apply (rule ballI)
    apply (rule trans[OF fun_cong[OF unfold1_o_dtor1] id_apply])
   apply (rule ballI)
   apply (rule trans[OF fun_cong[OF unfold2_o_dtor2] id_apply])
  apply (rule sym[OF id_apply])
  done

lemmas dtor1_ctor1 = pointfree_idE[OF dtor1_o_ctor1]
lemmas dtor2_ctor2 = pointfree_idE[OF dtor2_o_ctor2]
lemmas ctor1_dtor1 = pointfree_idE[OF ctor1_o_dtor1]
lemmas ctor2_dtor2 = pointfree_idE[OF ctor2_o_dtor2]

lemmas bij_dtor1 = o_bij[OF ctor1_o_dtor1 dtor1_o_ctor1]
lemmas inj_dtor1 = bij_is_inj[OF bij_dtor1]
lemmas surj_dtor1 = bij_is_surj[OF bij_dtor1]
lemmas dtor1_nchotomy = surjD[OF surj_dtor1]
lemmas dtor1_diff = inj_eq[OF inj_dtor1]
lemmas dtor1_cases = exE[OF dtor1_nchotomy]
lemmas bij_dtor2 = o_bij[OF ctor2_o_dtor2 dtor2_o_ctor2]
lemmas inj_dtor2 = bij_is_inj[OF bij_dtor2]
lemmas surj_dtor2 = bij_is_surj[OF bij_dtor2]
lemmas dtor2_nchotomy = surjD[OF surj_dtor2]
lemmas dtor2_diff = inj_eq[OF inj_dtor2]
lemmas dtor2_cases = exE[OF dtor2_nchotomy]

lemmas bij_ctor1 = o_bij[OF dtor1_o_ctor1 ctor1_o_dtor1]
lemmas inj_ctor1 = bij_is_inj[OF bij_ctor1]
lemmas surj_ctor1 = bij_is_surj[OF bij_ctor1]
lemmas ctor1_nchotomy = surjD[OF surj_ctor1]
lemmas ctor1_diff = inj_eq[OF inj_ctor1]
lemmas ctor1_cases = exE[OF ctor1_nchotomy]
lemmas bij_ctor2 = o_bij[OF dtor2_o_ctor2 ctor2_o_dtor2]
lemmas inj_ctor2 = bij_is_inj[OF bij_ctor2]
lemmas surj_ctor2 = bij_is_surj[OF bij_ctor2]
lemmas ctor2_nchotomy = surjD[OF surj_ctor2]
lemmas ctor2_diff = inj_eq[OF inj_ctor2]
lemmas ctor2_cases = exE[OF ctor2_nchotomy]

lemmas ctor1_unfold1 = iffD1[OF dtor1_diff trans[OF unfold1 sym[OF dtor1_ctor1]]]
lemmas ctor2_unfold2 = iffD1[OF dtor2_diff trans[OF unfold2 sym[OF dtor2_ctor2]]]

(* corecursor: *)

definition corec1 where "corec1 s1 s2 =
  unfold1 (case_sum (F1map id Inl Inl o dtor1) s1)
          (case_sum (F2map id Inl Inl o dtor2) s2) o Inr"
definition corec2 where "corec2 s1 s2 =
  unfold2 (case_sum (F1map id Inl Inl o dtor1) s1)
          (case_sum (F2map id Inl Inl o dtor2) s2) o Inr"

lemma dtor1_o_unfold1: "dtor1 o unfold1 s1 s2 = F1map id (unfold1 s1 s2) (unfold2 s1 s2) o s1"
  by (tactic ‹rtac @{context} (BNF_Tactics.mk_pointfree2 @{context} @{thm unfold1}) 1›)
lemma dtor2_o_unfold2: "dtor2 o unfold2 s1 s2 = F2map id (unfold1 s1 s2) (unfold2 s1 s2) o s2"
  by (tactic ‹rtac @{context} (BNF_Tactics.mk_pointfree2 @{context} @{thm unfold2}) 1›)

lemma corec1_Inl_sum:
  "unfold1 (case_sum (F1map id Inl Inl ∘ dtor1) s1) (case_sum (F2map id Inl Inl ∘ dtor2) s2) ∘ Inl = id"
  apply (rule trans[OF conjunct1[OF unfold_unique] unfold1_dtor])
   apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF F1.map_comp0[of id, unfolded id_o] refl]])
   apply (rule sym[OF trans[OF o_assoc]])
   apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF dtor1_o_unfold1 refl]])
   apply (rule box_equals[OF _ o_assoc o_assoc])
   apply (rule arg_cong2[of _ _ _ _ "(o)", OF refl case_sum_o_inj(1)])
  apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF F2.map_comp0[of id, unfolded id_o] refl]])
  apply (rule sym[OF trans[OF o_assoc]])
  apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF dtor2_o_unfold2 refl]])
  apply (rule box_equals[OF _ o_assoc o_assoc])
  apply (rule arg_cong2[of _ _ _ _ "(o)", OF refl case_sum_o_inj(1)])
  done

lemma corec2_Inl_sum:
  "unfold2 (case_sum (F1map id Inl Inl ∘ dtor1) s1) (case_sum (F2map id Inl Inl ∘ dtor2) s2) ∘ Inl = id"
  apply (rule trans[OF conjunct2[OF unfold_unique] unfold2_dtor])
   apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF F1.map_comp0[of id, unfolded id_o] refl]])
   apply (rule sym[OF trans[OF o_assoc]])
   apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF dtor1_o_unfold1 refl]])
   apply (rule box_equals[OF _ o_assoc o_assoc])
   apply (rule arg_cong2[of _ _ _ _ "(o)", OF refl case_sum_o_inj(1)])
  apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF F2.map_comp0[of id, unfolded id_o] refl]])
  apply (rule sym[OF trans[OF o_assoc]])
  apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF dtor2_o_unfold2 refl]])
  apply (rule box_equals[OF _ o_assoc o_assoc])
  apply (rule arg_cong2[of _ _ _ _ "(o)", OF refl case_sum_o_inj(1)])
  done

lemma case_sum_expand_Inr: "f o Inl = g ==> case_sum g (f o Inr) = f"
  by (auto split: sum.splits)

theorem corec1:
  "dtor1 (corec1 s1 s2 a) =
    F1map id (case_sum id (corec1 s1 s2)) (case_sum id (corec2 s1 s2)) (s1 a)"
  unfolding corec1_def corec2_def o_apply unfold1 sum.case
    case_sum_expand_Inr[OF corec1_Inl_sum] case_sum_expand_Inr[OF corec2_Inl_sum] ..

theorem corec2:
  "dtor2 (corec2 s1 s2 a) =
    F2map id (case_sum id (corec1 s1 s2)) (case_sum id (corec2 s1 s2)) (s2 a)"
  unfolding corec1_def corec2_def o_apply unfold2 sum.case
    case_sum_expand_Inr[OF corec1_Inl_sum] case_sum_expand_Inr[OF corec2_Inl_sum] ..

lemma corec_unique:
  "F1map id (case_sum id f1) (case_sum id f2) ∘ s1 = dtor1 ∘ f1 ==>
   F2map id (case_sum id f1) (case_sum id f2) ∘ s2 = dtor2 ∘ f2 ==>
   f1 = corec1 s1 s2 ∧ f2 = corec2 s1 s2"
  unfolding corec1_def corec2_def case_sum_expand_Inr'[OF corec1_Inl_sum] case_sum_expand_Inr'[OF corec2_Inl_sum]
  apply (rule unfold_unique)
   apply (unfold o_case_sum id_o o_id F1.map_comp0[symmetric] F2.map_comp0[symmetric]
      F1.map_id0 F2.map_id0 o_assoc case_sum_o_inj(1))
   apply (erule arg_cong2[of _ _ _ _ case_sum, OF refl])
  apply (erule arg_cong2[of _ _ _ _ case_sum, OF refl])
  done

subsection ‹Coinduction›

lemma Frel_coind:
  "[∀a b. phi1 a b ⟶ F1rel (=) phi1 phi2 (dtor1 a) (dtor1 b);
    ∀a b. phi2 a b ⟶ F2rel (=) phi1 phi2 (dtor2 a) (dtor2 b)] ==>
   (phi1 a1 b1 ⟶ a1 = b1) ∧ (phi2 a2 b2 ⟶ a2 = b2)"
  apply (rule rev_mp)
   apply (rule JF_cind)
   apply (rule iffD2)
    apply (rule bis_Frel)
   apply (rule conjI)

    apply (rule conjI)
     apply (rule ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]])
    apply (rule ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]])

   apply (rule conjI)
    apply (rule allI)+
    apply (rule impI)
    apply (erule allE)+
    apply (rule predicate2D[OF eq_refl[OF F1rel_cong]])
       apply (rule refl)
      apply (rule in_rel_Collect_case_prod_eq[symmetric])
     apply (rule in_rel_Collect_case_prod_eq[symmetric])
    apply (erule mp)
    apply (erule CollectE)
    apply (erule case_prodD)

   apply (rule allI)+
   apply (rule impI)
   apply (erule allE)+
   apply (rule predicate2D[OF eq_refl[OF F2rel_cong]])
      apply (rule refl)
     apply (rule in_rel_Collect_case_prod_eq[symmetric])
    apply (rule in_rel_Collect_case_prod_eq[symmetric])
   apply (erule mp)
   apply (erule CollectE)
   apply (erule case_prodD)


  apply (rule impI)
  apply (erule conjE)+

  apply (rule conjI)
   apply (rule impI)
   apply (rule IdD)
   apply (erule subsetD)
   apply (rule CollectI)
   apply (erule case_prodI)

  apply (rule impI)
  apply (rule IdD)
  apply (erule subsetD)
  apply (rule CollectI)
  apply (erule case_prodI)
  done

subsection ‹The Result as an BNF›

abbreviation JF1map where
  "JF1map u ≡ unfold1 (F1map u id id o dtor1) (F2map u id id o dtor2)"
abbreviation JF2map where
  "JF2map u ≡ unfold2 (F1map u id id o dtor1) (F2map u id id o dtor2)"

lemma JF1map: "dtor1 o JF1map u = F1map u (JF1map u) (JF2map u) o dtor1"
  apply (rule ext)
  apply (rule sym[OF trans[OF o_apply]])
  apply (rule sym[OF trans[OF o_apply]])
  apply (rule trans[OF unfold1])
  apply (rule box_equals[OF F1.map_comp _ F1.map_cong0, rotated])
     apply (rule fun_cong[OF id_o])
    apply (rule fun_cong[OF o_id])
   apply (rule fun_cong[OF o_id])
  apply (rule sym[OF arg_cong[OF o_apply]])
  done

lemma JF2map: "dtor2 o JF2map u = F2map u (JF1map u) (JF2map u) o dtor2"
  apply (rule ext)
  apply (rule sym[OF trans[OF o_apply]])
  apply (rule sym[OF trans[OF o_apply]])
  apply (rule trans[OF unfold2])
  apply (rule box_equals[OF F2.map_comp _ F2.map_cong0, rotated])
     apply (rule fun_cong[OF id_o])
    apply (rule fun_cong[OF o_id])
   apply (rule fun_cong[OF o_id])
  apply (rule sym[OF arg_cong[OF o_apply]])
  done

lemmas JF1map_simps = o_eq_dest[OF JF1map]
lemmas JF2map_simps = o_eq_dest[OF JF2map]

theorem JF1map_id: "JF1map id = id"
  apply (rule trans)
   apply (rule conjunct1)
   apply (rule unfold_unique)
    apply (rule sym[OF JF1map])
   apply (rule sym[OF JF2map])
  apply (rule unfold1_dtor)
  done

theorem JF2map_id: "JF2map id = id"
  apply (rule trans)
   apply (rule conjunct2)
   apply (rule unfold_unique)
    apply (rule sym[OF JF1map])
   apply (rule sym[OF JF2map])
  apply (rule unfold2_dtor)
  done

lemma JFmap_unique:
  "[dtor1 o u = F1map f u v o dtor1; dtor2 o v = F2map f u v o dtor2] ==>
    u = JF1map f ∧ v = JF2map f"
  apply (rule unfold_unique)
  unfolding o_assoc F1.map_comp0[symmetric] F2.map_comp0[symmetric] id_o o_id
   apply (erule sym)
  apply (erule sym)
  done

theorem JF1map_comp: "JF1map (g o f) = JF1map g o JF1map f"
  apply (rule sym)
  apply (rule conjunct1)
  apply (rule JFmap_unique)
   apply (rule trans[OF o_assoc])
   apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF JF1map refl]])
   apply (rule trans[OF sym[OF o_assoc]])
   apply (rule trans[OF arg_cong[OF JF1map]])
   apply (rule trans[OF o_assoc])
   apply (rule arg_cong2[of _ _ _ _ "(o)", OF sym[OF F1.map_comp0] refl])

  apply (rule trans[OF o_assoc])
  apply (rule trans[OF arg_cong2[of _ _ _ _ "(o)", OF JF2map refl]])
  apply (rule trans[OF sym[OF o_assoc]])
  apply (rule trans[OF arg_cong[OF JF2map]])
  apply (rule trans[OF o_assoc])
  apply (rule arg_cong2[of _ _ _ _ "(o)", OF sym[OF F2.map_comp0] refl])
  done

theorem JF2map_comp: "JF2map (g o f) = JF2map g o JF2map f"
  apply (rule sym)
  apply (rule conjunct2)
  apply (tactic ‹rtac @{context} (Thm.permute_prems 0 1 @{thm unfold_unique}) 1›)

   apply (rule trans[OF o_assoc])
   apply (rule trans[OF arg_cong[OF sym[OF F2.map_comp0]]])
   apply (rule sym[OF trans[OF o_assoc]])
   apply (rule trans[OF arg_cong2[OF JF2map refl]])
   apply (rule trans[OF sym[OF o_assoc]])
   apply (rule trans[OF arg_cong[OF JF2map]])
   apply (rule trans[OF o_assoc])
   apply (rule trans[OF arg_cong2[OF sym[OF F2.map_comp0] refl]])
   apply (rule ext)
   apply (rule trans[OF o_apply])
   apply (rule sym)
   apply (rule trans[OF o_apply])
   apply (rule F2.map_cong0)
     apply (rule trans[OF o_apply])
     apply (rule id_apply)
    apply (rule trans[OF o_apply])
    apply (rule arg_cong[OF id_apply])
   apply (rule trans[OF o_apply])
   apply (rule arg_cong[OF id_apply])

  apply (rule trans[OF o_assoc])
  apply (rule trans[OF arg_cong[OF sym[OF F1.map_comp0]]])
  apply (rule sym[OF trans[OF o_assoc]])
  apply (rule trans[OF arg_cong2[OF JF1map refl]])
  apply (rule trans[OF sym[OF o_assoc]])
  apply (rule trans[OF arg_cong[OF JF1map]])
  apply (rule trans[OF o_assoc])
  apply (rule trans[OF arg_cong2[OF sym[OF F1.map_comp0] refl]])
  apply (rule ext)
  apply (rule trans[OF o_apply])
  apply (rule sym)
  apply (rule trans[OF o_apply])
  apply (rule F1.map_cong0)
    apply (rule trans[OF o_apply])
    apply (rule id_apply)
   apply (rule trans[OF o_apply])
   apply (rule arg_cong[OF id_apply])
  apply (rule trans[OF o_apply])
  apply (rule arg_cong[OF id_apply])
  done

(* The hereditary F-sets1: *)
definition JFcol where
  "JFcol = rec_nat (%a. {}, %b. {})
     (%n rec.
     (%a. F1set1 (dtor1 a) ∪
       ((∪a' ∈ F1set2 (dtor1 a). fst rec a') ∪
       (∪a' ∈ F1set3 (dtor1 a). snd rec a')),
      %b. F2set1 (dtor2 b) ∪
       ((∪b' ∈ F2set2 (dtor2 b). fst rec b') ∪
       (∪b' ∈ F2set3 (dtor2 b). snd rec b'))))"

abbreviation JF1col where "JF1col n ≡ fst (JFcol n)"
abbreviation JF2col where "JF2col n ≡ snd (JFcol n)"

lemmas JF1col_0 = fun_cong[OF fstI[OF rec_nat_0_imp[OF JFcol_def]]]
lemmas JF2col_0 = fun_cong[OF sndI[OF rec_nat_0_imp[OF JFcol_def]]]
lemmas JF1col_Suc = fun_cong[OF fstI[OF rec_nat_Suc_imp[OF JFcol_def]]]
lemmas JF2col_Suc = fun_cong[OF sndI[OF rec_nat_Suc_imp[OF JFcol_def]]]

lemma JFcol_minimal:
  "[∧a. F1set1 (dtor1 a) ⊆ K1 a;
    ∧b. F2set1 (dtor2 b) ⊆ K2 b;
    ∧a a'. a' ∈ F1set2 (dtor1 a) ==> K1 a' ⊆ K1 a;
    ∧a b'. b' ∈ F1set3 (dtor1 a) ==> K2 b' ⊆ K1 a;
    ∧b a'. a' ∈ F2set2 (dtor2 b) ==> K1 a' ⊆ K2 b;
    ∧b b'. b' ∈ F2set3 (dtor2 b) ==> K2 b' ⊆ K2 b] ==>
  ∀a b. JF1col n a ⊆ K1 a ∧ JF2col n b ⊆ K2 b"
  apply (rule nat_induct)
   apply (rule allI)+
   apply (rule conjI)
    apply (rule ord_eq_le_trans)
     apply (rule JF1col_0)
    apply (rule empty_subsetI)

   apply (rule ord_eq_le_trans)
    apply (rule JF2col_0)
   apply (rule empty_subsetI)

  apply (rule allI)+
  apply (rule conjI)
   apply (rule ord_eq_le_trans)
    apply (rule JF1col_Suc)
   apply (rule Un_least)
    apply assumption
   apply (rule Un_least)
    apply (rule UN_least)
    apply (erule allE conjE)+
    apply (rule subset_trans)
     apply assumption
    apply assumption

   apply (rule UN_least)
   apply (erule allE conjE)+
   apply (rule subset_trans)
    apply assumption
   apply assumption

(**)

  apply (rule ord_eq_le_trans)
   apply (rule JF2col_Suc)
  apply (rule Un_least)
   apply assumption
  apply (rule Un_least)
   apply (rule UN_least)
   apply (erule allE conjE)+
   apply (rule subset_trans)
    apply assumption
   apply assumption

  apply (rule UN_least)
  apply (erule allE conjE)+
  apply (rule subset_trans)
   apply assumption
  apply assumption
  done

lemma JFset_minimal:
  "[∧a. F1set1 (dtor1 a) ⊆ K1 a;
    ∧b. F2set1 (dtor2 b) ⊆ K2 b;
    ∧a a'. a' ∈ F1set2 (dtor1 a) ==> K1 a' ⊆ K1 a;
    ∧a b'. b' ∈ F1set3 (dtor1 a) ==> K2 b' ⊆ K1 a;
    ∧b a'. a' ∈ F2set2 (dtor2 b) ==> K1 a' ⊆ K2 b;
    ∧b b'. b' ∈ F2set3 (dtor2 b) ==> K2 b' ⊆ K2 b] ==>
  (∪n. JF1col n a) ⊆ K1 a ∧ (∪n. JF2col n b) ⊆ K2 b"
  apply (rule conjI)
   apply (rule UN_least)
   apply (rule rev_mp)
    apply (rule JFcol_minimal)
         apply assumption
        apply assumption
       apply assumption
      apply assumption
     apply assumption
    apply assumption
   apply (rule impI)
   apply (erule allE conjE)+
   apply assumption

  apply (rule UN_least)
  apply (rule rev_mp)
   apply (rule JFcol_minimal)
        apply assumption
       apply assumption
      apply assumption
     apply assumption
    apply assumption
   apply assumption
  apply (rule impI)
  apply (erule allE conjE)+
  apply assumption
  done

abbreviation JF1set where "JF1set a ≡ (∪n. JF1col n a)"
abbreviation JF2set where "JF2set a ≡ (∪n. JF2col n a)"

lemma F1set1_incl_JF1set:
  "F1set1 (dtor1 a) ⊆ JF1set a"
  apply (rule SUP_upper2)
   apply (rule UNIV_I)
  apply (rule ord_le_eq_trans)
   apply (rule Un_upper1)
  apply (rule sym)
  apply (rule JF1col_Suc)
  done

lemma F2set1_incl_JF2set:
  "F2set1 (dtor2 a) ⊆ JF2set a"
  apply (rule SUP_upper2)
   apply (rule UNIV_I)
  apply (rule ord_le_eq_trans)
   apply (rule Un_upper1)
  apply (rule sym)
  apply (rule JF2col_Suc)
  done

lemma F1set2_JF1set_incl_JF1set:
  "a' ∈ F1set2 (dtor1 a) ==> JF1set a' ⊆ JF1set a"
  apply (rule UN_least)
  apply (rule subsetI)
  apply (rule UN_I)
   apply (rule UNIV_I)
  apply (rule subsetD)
   apply (rule equalityD2)
   apply (rule JF1col_Suc)
  apply (rule UnI2)
  apply (tactic ‹rtac @{context} (BNF_Util.mk_UnIN 2 1) 1›)
  apply (erule UN_I)
  apply assumption
  done

lemma F1set3_JF2set_incl_JF1set:
  "a' ∈ F1set3 (dtor1 a) ==> JF2set a' ⊆ JF1set a"
  apply (rule UN_least)
  apply (rule subsetI)
  apply (rule UN_I)
   apply (rule UNIV_I)
  apply (rule subsetD)
   apply (rule equalityD2)
   apply (rule JF1col_Suc)
  apply (rule UnI2)
  apply (tactic ‹rtac @{context} (BNF_Util.mk_UnIN 2 2) 1›)
  apply (erule UN_I)
  apply assumption
  done

lemma F2set2_JF1set_incl_JF2set:
  "a' ∈ F2set2 (dtor2 a) ==> JF1set a' ⊆ JF2set a"
  apply (rule UN_least)
  apply (rule subsetI)
  apply (rule UN_I)
   apply (rule UNIV_I)
  apply (rule subsetD)
   apply (rule equalityD2)
   apply (rule JF2col_Suc)
  apply (rule UnI2)
  apply (tactic ‹rtac @{context} (BNF_Util.mk_UnIN 2 1) 1›)
  apply (erule UN_I)
  apply assumption
  done

lemma F2set3_JF2set_incl_JF2set:
  "a' ∈ F2set3 (dtor2 a) ==> JF2set a' ⊆ JF2set a"
  apply (rule UN_least)
  apply (rule subsetI)
  apply (rule UN_I)
   apply (rule UNIV_I)
  apply (rule subsetD)
   apply (rule equalityD2)
   apply (rule JF2col_Suc)
  apply (rule UnI2)
  apply (tactic ‹rtac @{context} (BNF_Util.mk_UnIN 2 2) 1›)
  apply (erule UN_I)
  apply assumption
  done

lemmas F1set1_JF1set = subsetD[OF F1set1_incl_JF1set]
lemmas F2set1_JF2set = subsetD[OF F2set1_incl_JF2set]
lemmas F1set2_JF1set_JF1set = subsetD[OF F1set2_JF1set_incl_JF1set]
lemmas F1set3_JF2set_JF1set = subsetD[OF F1set3_JF2set_incl_JF1set]
lemmas F2set2_JF1set_JF2set = subsetD[OF F2set2_JF1set_incl_JF2set]
lemmas F2set3_JF2set_JF2set = subsetD[OF F2set3_JF2set_incl_JF2set]

lemma JFset_le:
  fixes a :: "'a JF1" and b :: "'a JF2"
  shows
    "JF1set a ⊆ F1set1 (dtor1 a) ∪ (∪ (JF1set ` F1set2 (dtor1 a)) ∪ ∪ (JF2set ` F1set3 (dtor1 a))) ∧
    JF2set b ⊆ F2set1 (dtor2 b) ∪ (∪ (JF1set ` F2set2 (dtor2 b)) ∪ ∪ (JF2set ` F2set3 (dtor2 b)))"
  apply (rule JFset_minimal)
       apply (rule Un_upper1)
      apply (rule Un_upper1)
     apply (rule subsetI)
     apply (rule UnI2)
     apply (tactic ‹rtac @{context} (BNF_Util.mk_UnIN 2 1) 1›)
     apply (erule UN_I)
     apply (erule UnE)
      apply (erule F1set1_JF1set)
     apply (erule UnE)+
      apply (erule UN_E)
      apply (erule F1set2_JF1set_JF1set)
      apply assumption
     apply (erule UN_E)
     apply (erule F1set3_JF2set_JF1set)
     apply assumption
    apply (rule subsetI)
    apply (rule UnI2)
    apply (tactic ‹rtac @{context} (BNF_Util.mk_UnIN 2 2) 1›)
    apply (erule UN_I)
    apply (erule UnE)
     apply (erule F2set1_JF2set)
    apply (erule UnE)+
     apply (erule UN_E)
     apply (erule F2set2_JF1set_JF2set)
     apply assumption
    apply (erule UN_E)
    apply (erule F2set3_JF2set_JF2set)
    apply assumption
   apply (rule subsetI)
   apply (rule UnI2)
   apply (tactic ‹rtac @{context} (BNF_Util.mk_UnIN 2 1) 1›)
   apply (erule UN_I)
   apply (erule UnE)+
    apply (erule F1set1_JF1set)
   apply (erule UnE)+
    apply (erule UN_E)
    apply (erule F1set2_JF1set_JF1set)
    apply assumption
   apply (erule UN_E)
   apply (erule F1set3_JF2set_JF1set)
   apply assumption
  apply (rule subsetI)
  apply (rule UnI2)
  apply (tactic ‹rtac @{context} (BNF_Util.mk_UnIN 2 2) 1›)
  apply (erule UN_I)
  apply (erule UnE)+
   apply (erule F2set1_JF2set)
  apply (erule UnE)+
   apply (erule UN_E)
   apply (erule F2set2_JF1set_JF2set)
   apply assumption
  apply (erule UN_E)
  apply (erule F2set3_JF2set_JF2set)
  apply assumption
  done

theorem JF1set_simps:
  "JF1set a = F1set1 (dtor1 a) ∪
    ((∪ b ∈ F1set2 (dtor1 a). JF1set b) ∪
     (∪ b ∈ F1set3 (dtor1 a). JF2set b))"
  apply (rule equalityI)
   apply (rule conjunct1[OF JFset_le])
  apply (rule Un_least)
   apply (rule F1set1_incl_JF1set)
  apply (rule Un_least)
   apply (rule UN_least)
   apply (erule F1set2_JF1set_incl_JF1set)
  apply (rule UN_least)
  apply (erule F1set3_JF2set_incl_JF1set)
  done

theorem JF2set_simps:
  "JF2set a = F2set1 (dtor2 a) ∪
    ((∪ b ∈ F2set2 (dtor2 a). JF1set b) ∪
     (∪ b ∈ F2set3 (dtor2 a). JF2set b))"
  apply (rule equalityI)
   apply (rule conjunct2[OF JFset_le])
  apply (rule Un_least)
   apply (rule F2set1_incl_JF2set)
  apply (rule Un_least)
   apply (rule UN_least)
   apply (erule F2set2_JF1set_incl_JF2set)
  apply (rule UN_least)
  apply (erule F2set3_JF2set_incl_JF2set)
  done

lemma JFcol_natural:
  "∀b1 b2. u ` (JF1col n b1) = JF1col n (JF1map u b1) ∧
           u ` (JF2col n b2) = JF2col n (JF2map u b2)"
  apply (rule nat_induct)
   apply (rule allI)+
  unfolding JF1col_0 JF2col_0
   apply (rule conjI)
    apply (rule image_empty)
   apply (rule image_empty)

  apply (rule allI)+
  apply (rule conjI)
   apply (unfold JF1col_Suc JF1map_simps image_Un image_UN UN_simps(10)
      F1.set_map(1) F1.set_map(2) F1.set_map(3)) [1]
   apply (rule arg_cong2[of _ _ _ _ "(∪)"])
    apply (rule refl)
   apply (rule arg_cong2[of _ _ _ _ "(∪)"])
    apply (rule SUP_cong[OF refl])
    apply (erule allE)+
    apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (rule SUP_cong[OF refl])
   apply (erule allE)+
   apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)

  apply (unfold JF2col_Suc JF2map_simps image_Un image_UN UN_simps(10)
      F2.set_map(1) F2.set_map(2) F2.set_map(3)) [1]
  apply (rule arg_cong2[of _ _ _ _ "(∪)"])
   apply (rule refl)
  apply (rule arg_cong2[of _ _ _ _ "(∪)"])
   apply (rule SUP_cong[OF refl])
   apply (erule allE)+
   apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
  apply (rule SUP_cong[OF refl])
  apply (erule allE)+
  apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  done

theorem JF1set_natural: "JF1set o (JF1map u) = image u o JF1set"
  apply (rule ext)
  apply (rule trans[OF o_apply])
  apply (rule sym)
  apply (rule trans[OF o_apply])
  apply (rule trans[OF image_UN])
  apply (rule SUP_cong[OF refl])
  apply (rule conjunct1)
  apply (rule spec[OF spec[OF JFcol_natural]])
  done

theorem JF2set_natural: "JF2set o (JF2map u) = image u o JF2set"
  apply (rule ext)
  apply (rule trans[OF o_apply])
  apply (rule sym)
  apply (rule trans[OF o_apply])
  apply (rule trans[OF image_UN])
  apply (rule SUP_cong[OF refl])
  apply (rule conjunct2)
  apply (rule spec[OF spec[OF JFcol_natural]])
  done

theorem JFmap_cong0:
  "((∀p ∈ JF1set a. u p = v p) ⟶ JF1map u a = JF1map v a) ∧
   ((∀p ∈ JF2set b. u p = v p) ⟶ JF2map u b = JF2map v b)"
  apply (rule rev_mp)
   apply (rule Frel_coind[of
        "%b c. ∃a. a ∈ {a. ∀p ∈ JF1set a. u p = v p} ∧ b = JF1map u a ∧ c = JF1map v a"
        "%b c. ∃a. a ∈ {a. ∀p ∈ JF2set a. u p = v p} ∧ b = JF2map u a ∧ c = JF2map v a"])
    apply (intro allI impI iffD2[OF F1.in_rel])

    apply (erule exE conjE)+
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (rule exI)

    apply (rule conjI[rotated])
     apply (rule conjI)
      apply (rule trans[OF F1.map_comp])
      apply (rule sym)
      apply (rule trans[OF JF1map_simps])
      apply (rule F1.map_cong0)
        apply (rule sym[OF trans[OF o_apply]])
        apply (rule fst_conv)
       apply (rule sym[OF fun_cong[OF fst_convol[unfolded convol_def]]])
      apply (rule sym[OF fun_cong[OF fst_convol[unfolded convol_def]]])

     apply (rule trans[OF F1.map_comp])
     apply (rule sym)
     apply (rule trans[OF JF1map_simps])
     apply (rule F1.map_cong0)
       apply (rule sym[OF trans[OF o_apply]])
       apply (rule trans[OF snd_conv])
       apply (erule CollectE)
       apply (erule bspec)
       apply (erule F1set1_JF1set)
      apply (rule sym[OF fun_cong[OF snd_convol[unfolded convol_def]]])
     apply (rule sym[OF fun_cong[OF snd_convol[unfolded convol_def]]])

    apply (rule CollectI)
    apply (rule conjI)
     apply (rule ord_eq_le_trans)
      apply (rule F1.set_map(1))
     apply (rule image_subsetI)
     apply (rule CollectI)
     apply (rule case_prodI)
     apply (rule refl)

    apply (rule conjI)
     apply (rule ord_eq_le_trans)
      apply (rule F1.set_map(2))
     apply (rule image_subsetI)
     apply (rule CollectI)
     apply (rule case_prodI)
     apply (rule exI)
     apply (rule conjI)
      apply (rule CollectI)
      apply (rule ballI)
      apply (erule CollectE)
      apply (erule bspec)
      apply (erule F1set2_JF1set_JF1set)
      apply assumption
     apply (rule conjI[OF refl refl])

    apply (rule ord_eq_le_trans)
     apply (rule F1.set_map(3))
    apply (rule image_subsetI)
    apply (rule CollectI)
    apply (rule case_prodI)
    apply (rule exI)
    apply (rule conjI)
     apply (rule CollectI)
     apply (rule ballI)
     apply (erule CollectE)
     apply (erule bspec)
     apply (erule F1set3_JF2set_JF1set)
     apply assumption
    apply (rule conjI[OF refl refl])


(**)

   apply (intro allI impI iffD2[OF F2.in_rel])

   apply (erule exE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule exI)

   apply (rule conjI[rotated])
    apply (rule conjI)
     apply (rule trans[OF F2.map_comp])
     apply (rule sym)
     apply (rule trans[OF JF2map_simps])
     apply (rule F2.map_cong0)
       apply (rule sym[OF trans[OF o_apply]])
       apply (rule fst_conv)
      apply (rule sym[OF fun_cong[OF fst_convol[unfolded convol_def]]])
     apply (rule sym[OF fun_cong[OF fst_convol[unfolded convol_def]]])

    apply (rule trans[OF F2.map_comp])
    apply (rule sym)
    apply (rule trans[OF JF2map_simps])
    apply (rule F2.map_cong0)
      apply (rule sym[OF trans[OF o_apply]])
      apply (rule trans[OF snd_conv])
      apply (erule CollectE)
      apply (erule bspec)
      apply (erule F2set1_JF2set)
     apply (rule sym[OF fun_cong[OF snd_convol[unfolded convol_def]]])
    apply (rule sym[OF fun_cong[OF snd_convol[unfolded convol_def]]])

   apply (rule CollectI)
   apply (rule conjI)
    apply (rule ord_eq_le_trans)
     apply (rule F2.set_map(1))
    apply (rule image_subsetI)
    apply (rule CollectI)
    apply (rule case_prodI)
    apply (rule refl)

   apply (rule conjI)
    apply (rule ord_eq_le_trans)
     apply (rule F2.set_map(2))
    apply (rule image_subsetI)
    apply (rule CollectI)
    apply (rule case_prodI)
    apply (rule exI)
    apply (rule conjI)
     apply (rule CollectI)
     apply (rule ballI)
     apply (erule CollectE)
     apply (erule bspec)
     apply (erule F2set2_JF1set_JF2set)
     apply assumption
    apply (rule conjI[OF refl refl])

   apply (rule ord_eq_le_trans)
    apply (rule F2.set_map(3))
   apply (rule image_subsetI)
   apply (rule CollectI)
   apply (rule case_prodI)
   apply (rule exI)
   apply (rule conjI)
    apply (rule CollectI)
    apply (rule ballI)
    apply (erule CollectE)
    apply (erule bspec)
    apply (erule F2set3_JF2set_JF2set)
    apply assumption
   apply (rule conjI[OF refl refl])

(**)

  apply (rule impI)

  apply (rule conjI)
   apply (rule impI)
   apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
   apply (erule mp)
   apply (rule exI)
   apply (rule conjI)
    apply (erule CollectI)
   apply (rule conjI)
    apply (rule refl)
   apply (rule refl)

  apply (rule impI)
  apply (tactic ‹dtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (erule mp)
  apply (rule exI)
  apply (rule conjI)
   apply (erule CollectI)
  apply (rule conjI)
   apply (rule refl)
  apply (rule refl)
  done

lemmas JF1map_cong0 = mp[OF conjunct1[OF JFmap_cong0]]
lemmas JF2map_cong0 = mp[OF conjunct2[OF JFmap_cong0]]

lemma JFcol_bd: "∀(j1 :: 'a JF1) (j2 :: 'a JF2). |JF1col n j1| <o bd_F ∧ |JF2col n j2| <o bd_F"
  apply (rule nat_induct)
   apply (rule allI)+
   apply (rule conjI)
    apply (rule ordIso_ordLess_trans)
     apply (rule card_of_ordIso_subst)
     apply (rule JF1col_0)
    apply (rule Cinfinite_gt_empty)
    apply (rule bd_F_Cinfinite)
   apply (rule ordIso_ordLess_trans)
    apply (rule card_of_ordIso_subst)
    apply (rule JF2col_0)
   apply (rule Cinfinite_gt_empty)
   apply (rule bd_F_Cinfinite)

  apply (rule allI)+
  apply (rule conjI)
   apply (rule ordIso_ordLess_trans)
    apply (rule card_of_ordIso_subst)
    apply (rule JF1col_Suc)
   apply (rule Un_Cinfinite_bound_strict)
     apply (rule F1set1_bd')
    apply (rule Un_Cinfinite_bound_strict)
      apply (rule regularCard_UNION_bound)
         apply (rule bd_F_Cinfinite)
        apply (rule bd_F_regularCard)
       apply (rule F1set2_bd')
      apply (erule allE)+
      apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
     apply (rule regularCard_UNION_bound)
        apply (rule bd_F_Cinfinite)
       apply (rule bd_F_regularCard)
      apply (rule F1set3_bd')
     apply (erule allE)+
     apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
    apply (rule bd_F_Cinfinite)
   apply (rule bd_F_Cinfinite)

  apply (rule ordIso_ordLess_trans)
   apply (rule card_of_ordIso_subst)
   apply (rule JF2col_Suc)
  apply (rule Un_Cinfinite_bound_strict)
    apply (rule F2set1_bd')
   apply (rule Un_Cinfinite_bound_strict)
     apply (rule regularCard_UNION_bound)
        apply (rule bd_F_Cinfinite)
       apply (rule bd_F_regularCard)
      apply (rule F2set2_bd')
     apply (erule allE)+
     apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
    apply (rule regularCard_UNION_bound)
       apply (rule bd_F_Cinfinite)
      apply (rule bd_F_regularCard)
     apply (rule F2set3_bd')
    apply (erule allE)+
    apply (tactic ‹etac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
   apply (rule bd_F_Cinfinite)
  apply (rule bd_F_Cinfinite)
  done

theorem JF1set_bd: "|JF1set j| <o bd_F"
  apply (rule regularCard_UNION_bound)
     apply (rule bd_F_Cinfinite)
    apply (rule bd_F_regularCard)
   apply (rule ordIso_ordLess_trans)
    apply (rule card_of_nat)
   apply (rule ordLess_ordIso_trans)
    apply (rule natLeq_ordLess_cinfinite)
     apply (rule sum_Cinfinite)
    apply (rule sum_card_order)
   apply (rule bd_F)
  apply (tactic ‹rtac @{context} (BNF_Util.mk_conjunctN 2 1) 1›)
  apply (rule spec[OF spec[OF JFcol_bd]])
  done

theorem JF2set_bd: "|JF2set j| <o bd_F"
  apply (rule regularCard_UNION_bound)
     apply (rule bd_F_Cinfinite)
    apply (rule bd_F_regularCard)
   apply (rule ordIso_ordLess_trans)
    apply (rule card_of_nat)
   apply (rule ordLess_ordIso_trans)
    apply (rule natLeq_ordLess_cinfinite)
     apply (rule sum_Cinfinite)
    apply (rule sum_card_order)
   apply (rule bd_F)
  apply (tactic ‹rtac @{context} (BNF_Util.mk_conjunctN 2 2) 1›)
  apply (rule spec[OF spec[OF JFcol_bd]])
  done

abbreviation "JF2wit ≡ ctor2 wit_F2"

theorem JF2wit: "∧x. x ∈ JF2set JF2wit ==> False"
  apply (drule rev_subsetD)
   apply (rule equalityD1)
   apply (rule JF2set_simps)
  unfolding dtor2_ctor2
  apply (erule UnE)
   apply (erule F2.wit)
  apply (erule UnE)
   apply (erule UN_E)
   apply (erule F2.wit)
  apply (erule UN_E)
  apply (erule F2.wit)
  done

abbreviation "JF1wit ≡ (%a. ctor1 (wit2_F1 a JF2wit))"

theorem JF1wit: "∧x. x ∈ JF1set (JF1wit a) ==> x = a"
  apply (drule rev_subsetD)
   apply (rule equalityD1)
   apply (rule JF1set_simps)
  unfolding dtor1_ctor1
  apply (erule UnE)+
   apply (erule F1.wit2)
  apply (erule UnE)
   apply (erule UN_E)
   apply (drule F1.wit2)
   apply (erule FalseE)
  apply (erule UN_E)
  apply (drule F1.wit2)
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (drule rev_subsetD)
   apply (rule equalityD1)
   apply (rule JF2set_simps)
  unfolding dtor2_ctor2
  apply (erule UnE)+
   apply (drule F2.wit)
   apply (erule FalseE)
  apply (erule UnE)
   apply (erule UN_E)
   apply (drule F2.wit)
   apply (erule FalseE)
  apply (erule UN_E)
  apply (drule F2.wit)
  apply (erule FalseE)
  done

(* Additions: *)

context
  fixes phi1 :: "'a ==> 'a JF1 ==> bool" and phi2 :: "'a ==> 'a JF2 ==> bool"
begin

lemmas JFset_induct =
  JFset_minimal[of "%b1. {a ∈ JF1set b1 . phi1 a b1}" "%b2. {a ∈ JF2set b2 . phi2 a b2}",
    unfolded subset_Collect_iff[OF F1set1_incl_JF1set] subset_Collect_iff[OF F2set1_incl_JF2set]
    subset_Collect_iff[OF subset_refl],
    OF ballI ballI
    subset_CollectI[OF F1set2_JF1set_incl_JF1set]
    subset_CollectI[OF F1set3_JF2set_incl_JF1set]
    subset_CollectI[OF F2set2_JF1set_incl_JF2set]
    subset_CollectI[OF F2set3_JF2set_incl_JF2set]]

end

(*export that one!*)
ML ‹rule_by_tactic @{context} (ALLGOALS (TRY o etac @{context} asm_rl)) @{thm JFset_induct}›

(* Compositionality of relators *)

abbreviation JF1in where "JF1in B ≡ {a. JF1set a ⊆ B}"
abbreviation JF2in where "JF2in B ≡ {a. JF2set a ⊆ B}"

(* Notions and facts that make sense for any BNF: *)
definition JF1rel where
  "JF1rel R = (BNF_Def.Grp (JF1in (Collect (case_prod R))) (JF1map fst))^--1 OO
              (BNF_Def.Grp (JF1in (Collect (case_prod R))) (JF1map snd))"

definition JF2rel where
  "JF2rel R = (BNF_Def.Grp (JF2in (Collect (case_prod R))) (JF2map fst))^--1 OO
              (BNF_Def.Grp (JF2in (Collect (case_prod R))) (JF2map snd))"

lemma in_JF1rel:
  "JF1rel R x y ⟷ (∃ z. z ∈ JF1in (Collect (case_prod R)) ∧ JF1map fst z = x ∧ JF1map snd z = y)"
  by (rule predicate2_eqD[OF trans[OF JF1rel_def OO_Grp_alt]])


lemma in_JF2rel:
  "JF2rel R x y ⟷ (∃ z. z ∈ JF2in (Collect (case_prod R)) ∧ JF2map fst z = x ∧ JF2map snd z = y)"
  by (rule predicate2_eqD[OF trans[OF JF2rel_def OO_Grp_alt]])

lemma J_rel_coind_ind:
  "[∀x y. R2 x y ⟶ (f x y ∈ F1in (Collect (case_prod R1)) (Collect (case_prod R2)) (Collect (case_prod R3)) ∧
                               F1map fst fst fst (f x y) = dtor1 x ∧
                               F1map snd snd snd (f x y) = dtor1 y);
   ∀x y. R3 x y ⟶ (g x y ∈ F2in (Collect (case_prod R1)) (Collect (case_prod R2)) (Collect (case_prod R3)) ∧
                               F2map fst fst fst (g x y) = dtor2 x ∧
                               F2map snd snd snd (g x y) = dtor2 y)] ==>
  (∀a∈JF1set z1. ∀x y. R2 x y ∧ z1 = unfold1 (case_prod f) (case_prod g) (x, y) ⟶ R1 (fst a) (snd a)) ∧
  (∀a∈JF2set z2. ∀x y. R3 x y ∧ z2 = unfold2 (case_prod f) (case_prod g) (x, y) ⟶ R1 (fst a) (snd a))"
  apply (tactic ‹rtac @{context} (rule_by_tactic @{context} (ALLGOALS (TRY o etac @{context} asm_rl))
 @{thm JFset_induct[of
 "λa z1. ∀x y. R2 x y ∧ z1 = unfold1 (case_prod f) (case_prod g) (x, y) ⟶ R1 (fst a) (snd a)"
 "λa z2. ∀x y. R3 x y ∧ z2 = unfold2 (case_prod f) (case_prod g) (x, y) ⟶ R1 (fst a) (snd a)"
 z1 z2]}) 1›)
       apply (rule allI impI)+
       apply (erule conjE)
       apply (drule spec2)
       apply (erule thin_rl)
       apply (drule mp)
        apply assumption
       apply (erule CollectE conjE Collect_case_prodD[OF subsetD] rev_subsetD)+
       apply hypsubst
  unfolding unfold1 F1.set_map(1) prod.case image_id id_apply
       apply (rule subset_refl)

      apply (rule allI impI)+
      apply (erule conjE)
      apply (erule thin_rl)
      apply (drule spec2)
      apply (drule mp)
       apply assumption
      apply (erule CollectE conjE Collect_case_prodD[OF subsetD] rev_subsetD)+
      apply hypsubst
  unfolding unfold2 F2.set_map(1) prod.case image_id id_apply
      apply (rule subset_refl)

(**)

     apply (rule impI allI)+
     apply (erule conjE)
     apply (drule spec2)
     apply (erule thin_rl)
     apply (drule mp)
      apply assumption
     apply (erule CollectE conjE)+
     apply (tactic ‹hyp_subst_tac @{context} 1›)
  unfolding unfold1 F1.set_map(2) prod.case image_id id_apply
     apply (erule imageE)
     apply (tactic ‹hyp_subst_tac @{context} 1›)
     apply (erule allE mp)+
     apply (rule conjI)
      apply (erule Collect_case_prodD[OF subsetD])
      apply assumption
     apply (rule arg_cong[OF surjective_pairing])
    (**)

    apply (rule impI allI)+
    apply (erule conjE)
    apply (drule spec2)
    apply (erule thin_rl)
    apply (drule mp)
     apply assumption
    apply (erule CollectE conjE)+
    apply (tactic ‹hyp_subst_tac @{context} 1›)
  unfolding unfold1 F1.set_map(3) prod.case image_id id_apply
    apply (erule imageE)
    apply (tactic ‹hyp_subst_tac @{context} 1›)
    apply (erule allE mp)+
    apply (rule conjI)
     apply (erule Collect_case_prodD[OF subsetD])
     apply assumption
    apply (rule arg_cong[OF surjective_pairing])

(**)

   apply (rule impI allI)+
   apply (erule conjE)
   apply (erule thin_rl)
   apply (drule spec2)
   apply (drule mp)
    apply assumption
   apply (erule CollectE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
  unfolding unfold2 F2.set_map(2) prod.case image_id id_apply
   apply (erule imageE)
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (erule allE mp)+
   apply (rule conjI)
    apply (erule Collect_case_prodD[OF subsetD])
    apply assumption
   apply (rule arg_cong[OF surjective_pairing])
    (**)

  apply (rule impI allI)+
  apply (erule conjE)
  apply (erule thin_rl)
  apply (drule spec2)
  apply (drule mp)
   apply assumption
  apply (erule CollectE conjE)+
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  unfolding unfold2 F2.set_map(3) prod.case image_id id_apply
  apply (erule imageE)
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (erule allE mp)+
  apply (rule conjI)
   apply (erule Collect_case_prodD[OF subsetD])
   apply assumption
  apply (rule arg_cong[OF surjective_pairing])
  done

lemma J_rel_coind_coind1:
  "[∀x y. R2 x y ⟶ (f x y ∈ F1in (Collect (case_prod R1)) (Collect (case_prod R2)) (Collect (case_prod R3)) ∧
                               F1map fst fst fst (f x y) = dtor1 x ∧
                               F1map snd snd snd (f x y) = dtor1 y);
   ∀x y. R3 x y ⟶ (g x y ∈ F2in (Collect (case_prod R1)) (Collect (case_prod R2)) (Collect (case_prod R3)) ∧
                               F2map fst fst fst (g x y) = dtor2 x ∧
                               F2map snd snd snd (g x y) = dtor2 y)] ==>
  ((∃y. R2 x1 y ∧ x1' = JF1map fst (unfold1 (case_prod f) (case_prod g) (x1, y))) ⟶ x1' = x1) ∧
  ((∃y. R3 x2 y ∧ x2' = JF2map fst (unfold2 (case_prod f) (case_prod g) (x2, y))) ⟶ x2' = x2)"
  apply (rule Frel_coind[of
        "λx1' x1. ∃y. R2 x1 y ∧ x1' = JF1map fst (unfold1 (case_prod f) (case_prod g) (x1, y))"
        "λx2' x2. ∃y. R3 x2 y ∧ x2' = JF2map fst (unfold2 (case_prod f) (case_prod g) (x2, y))"
        x1' x1
        x2' x2
        ])
   apply (intro allI impI iffD2[OF F1.in_rel])

   apply (erule exE conjE)+
   apply (drule spec2)
   apply (erule thin_rl)
   apply (drule mp)
    apply assumption
   apply (erule CollectE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule exI)
   apply (rule conjI[rotated])
    apply (rule conjI)
     apply (rule trans[OF F1.map_comp])
     apply (rule sym[OF trans[OF JF1map_simps]])
     apply (rule trans[OF arg_cong[OF unfold1]])
     apply (rule trans[OF F1.map_comp F1.map_cong0])
       apply (rule trans[OF fun_cong[OF o_id]])
       apply (rule sym[OF fun_cong[OF fst_diag_fst]])
      apply (rule sym[OF trans[OF o_apply]])
      apply (rule fst_conv)
     apply (rule sym[OF trans[OF o_apply]])
     apply (rule fst_conv)
    apply (rule trans[OF F1.map_comp])
    apply (rule trans[OF F1.map_cong0])
       apply (rule fun_cong[OF snd_diag_fst])
      apply (rule trans[OF o_apply])
      apply (rule snd_conv)
     apply (rule trans[OF o_apply])
     apply (rule snd_conv)
    apply (erule trans[OF arg_cong[OF prod.case]])

   apply (unfold prod.case o_def fst_conv snd_conv) []
   apply (rule CollectI)
   apply (rule conjI)
    apply (rule ord_eq_le_trans[OF F1.set_map(1)])
    apply (rule image_subsetI CollectI case_prodI)+
    apply (rule refl)

   apply (rule conjI)
    apply (rule ord_eq_le_trans[OF F1.set_map(2)])
    apply (rule image_subsetI CollectI case_prodI exI)+
    apply (rule conjI)
     apply (erule Collect_case_prodD[OF subsetD])
     apply assumption
    apply (rule arg_cong[OF surjective_pairing])

   apply (rule ord_eq_le_trans[OF F1.set_map(3)])
   apply (rule image_subsetI CollectI case_prodI exI)+
   apply (rule conjI)
    apply (erule Collect_case_prodD[OF subsetD])
    apply assumption
   apply (rule arg_cong[OF surjective_pairing])

(**)

  apply (intro allI impI iffD2[OF F2.in_rel])

  apply (erule exE conjE)+
  apply (erule thin_rl)
  apply (drule spec2)
  apply (drule mp)
   apply assumption
  apply (erule CollectE conjE)+
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (rule exI)
  apply (rule conjI[rotated])
   apply (rule conjI)
    apply (rule trans[OF F2.map_comp])
    apply (rule sym[OF trans[OF JF2map_simps]])
    apply (rule trans[OF arg_cong[OF unfold2]])
    apply (rule trans[OF F2.map_comp F2.map_cong0])
      apply (rule fun_cong[OF trans[OF o_id fst_diag_fst[symmetric]]])
     apply (rule sym[OF trans[OF o_apply]])
     apply (rule fst_conv)
    apply (rule sym[OF trans[OF o_apply]])
    apply (rule fst_conv)
   apply (rule trans[OF F2.map_comp])
   apply (rule trans[OF F2.map_cong0])
      apply (rule fun_cong[OF snd_diag_fst])
     apply (rule trans[OF o_apply])
     apply (rule snd_conv)
    apply (rule trans[OF o_apply])
    apply (rule snd_conv)
   apply (erule trans[OF arg_cong[OF prod.case]])

  apply (unfold prod.case o_def fst_conv snd_conv) []
  apply (rule CollectI)
  apply (rule conjI)
   apply (rule ord_eq_le_trans[OF F2.set_map(1)])
   apply (rule image_subsetI)
   apply (rule CollectI)
   apply (rule case_prodI)
   apply (rule refl)

  apply (rule conjI)
   apply (rule ord_eq_le_trans[OF F2.set_map(2)])
   apply (rule image_subsetI)
   apply (rule CollectI)
   apply (rule case_prodI)
   apply (rule exI)
   apply (rule conjI)
    apply (erule Collect_case_prodD[OF subsetD])
    apply assumption
   apply (rule arg_cong[OF surjective_pairing])

  apply (rule ord_eq_le_trans[OF F2.set_map(3)])
  apply (rule image_subsetI CollectI case_prodI exI)+
  apply (rule conjI)
   apply (erule Collect_case_prodD[OF subsetD])
   apply assumption
  apply (rule arg_cong[OF surjective_pairing])
  done

lemma J_rel_coind_coind2:
  "[∀x y. R2 x y ⟶ (f x y ∈ F1in (Collect (case_prod R1)) (Collect (case_prod R2)) (Collect (case_prod R3)) ∧
                               F1map fst fst fst (f x y) = dtor1 x ∧
                               F1map snd snd snd (f x y) = dtor1 y);
   ∀x y. R3 x y ⟶ (g x y ∈ F2in (Collect (case_prod R1)) (Collect (case_prod R2)) (Collect (case_prod R3)) ∧
                               F2map fst fst fst (g x y) = dtor2 x ∧
                               F2map snd snd snd (g x y) = dtor2 y)] ==>
  ((∃x. R2 x y1 ∧ y1' = JF1map snd (unfold1 (case_prod f) (case_prod g) (x, y1))) ⟶ y1' = y1) ∧
  ((∃x. R3 x y2 ∧ y2' = JF2map snd (unfold2 (case_prod f) (case_prod g) (x, y2))) ⟶ y2' = y2)"
  apply (rule Frel_coind[of
        "λy1' y1. ∃x. R2 x y1 ∧ y1' = JF1map snd (unfold1 (case_prod f) (case_prod g) (x, y1))"
        "λy2' y2. ∃x. R3 x y2 ∧ y2' = JF2map snd (unfold2 (case_prod f) (case_prod g) (x, y2))"
        y1' y1
        y2' y2
        ])
   apply (intro allI impI iffD2[OF F1.in_rel])

   apply (erule exE conjE)+
   apply (drule spec2)
   apply (erule thin_rl)
   apply (drule mp)
    apply assumption
   apply (erule CollectE conjE)+
   apply (tactic ‹hyp_subst_tac @{context} 1›)
   apply (rule exI)
   apply (rule conjI[rotated])
    apply (rule conjI)
     apply (rule trans[OF F1.map_comp])
     apply (rule sym[OF trans[OF JF1map_simps]])
     apply (rule trans[OF arg_cong[OF unfold1]])
     apply (rule trans[OF F1.map_comp F1.map_cong0])
       apply (rule trans[OF fun_cong[OF o_id]])
       apply (rule sym[OF fun_cong[OF fst_diag_snd]])
      apply (rule sym[OF trans[OF o_apply]])
      apply (rule fst_conv)
     apply (rule sym[OF trans[OF o_apply]])
     apply (rule fst_conv)
    apply (rule trans[OF F1.map_comp])
    apply (rule trans[OF F1.map_cong0])
       apply (rule fun_cong[OF snd_diag_snd])
      apply (rule trans[OF o_apply])
      apply (rule snd_conv)
     apply (rule trans[OF o_apply])
     apply (rule snd_conv)
    apply (erule trans[OF arg_cong[OF prod.case]])

   apply (unfold prod.case o_def fst_conv snd_conv) []
   apply (rule CollectI)
   apply (rule conjI)
    apply (rule ord_eq_le_trans[OF F1.set_map(1)])
    apply (rule image_subsetI CollectI case_prodI)+
    apply (rule refl)

   apply (rule conjI)
    apply (rule ord_eq_le_trans[OF F1.set_map(2)])
    apply (rule image_subsetI CollectI case_prodI exI)+
    apply (rule conjI)
     apply (erule Collect_case_prodD[OF subsetD])
     apply assumption
    apply (rule arg_cong[OF surjective_pairing])

   apply (rule ord_eq_le_trans[OF F1.set_map(3)])
   apply (rule image_subsetI CollectI case_prodI exI)+
   apply (rule conjI)
    apply (erule Collect_case_prodD[OF subsetD])
    apply assumption
   apply (rule arg_cong[OF surjective_pairing])

(**)

  apply (intro allI impI iffD2[OF F2.in_rel])

  apply (erule exE conjE)+
  apply (erule thin_rl)
  apply (drule spec2)
  apply (drule mp)
   apply assumption
  apply (erule CollectE conjE)+
  apply (tactic ‹hyp_subst_tac @{context} 1›)
  apply (rule exI)
  apply (rule conjI[rotated])
   apply (rule conjI)
    apply (rule trans[OF F2.map_comp])
    apply (rule sym[OF trans[OF JF2map_simps]])
    apply (rule trans[OF arg_cong[OF unfold2]])
    apply (rule trans[OF F2.map_comp F2.map_cong0])
      apply (rule trans[OF fun_cong[OF o_id]])
      apply (rule sym[OF fun_cong[OF fst_diag_snd]])
     apply (rule sym[OF trans[OF o_apply]])
     apply (rule fst_conv)
    apply (rule sym[OF trans[OF o_apply]])
    apply (rule fst_conv)
   apply (rule trans[OF F2.map_comp])
   apply (rule trans[OF F2.map_cong0])
      apply (rule fun_cong[OF snd_diag_snd])
     apply (rule trans[OF o_apply])
     apply (rule snd_conv)
    apply (rule trans[OF o_apply])
    apply (rule snd_conv)
   apply (erule trans[OF arg_cong[OF prod.case]])

  apply (unfold prod.case o_def fst_conv snd_conv) []
  apply (rule CollectI)
  apply (rule conjI)
   apply (rule ord_eq_le_trans[OF F2.set_map(1)])
   apply (rule image_subsetI CollectI case_prodI)+
   apply (rule refl)

  apply (rule conjI)
   apply (rule ord_eq_le_trans[OF F2.set_map(2)])
   apply (rule image_subsetI CollectI case_prodI exI)+
   apply (rule conjI)
    apply (erule Collect_case_prodD[OF subsetD])
    apply assumption
   apply (rule arg_cong[OF surjective_pairing])

  apply (rule ord_eq_le_trans[OF F2.set_map(3)])
  apply (rule image_subsetI CollectI case_prodI exI)+
  apply (rule conjI)
   apply (erule Collect_case_prodD[OF subsetD])
   apply assumption
  apply (rule arg_cong[OF surjective_pairing])
  done

lemma J_rel_coind:
  assumes CIH1: "∀x2 y2. R2 x2 y2 ⟶ F1rel R1 R2 R3 (dtor1 x2) (dtor1 y2)"
    and     CIH2: "∀x3 y3. R3 x3 y3 ⟶ F2rel R1 R2 R3 (dtor2 x3) (dtor2 y3)"
  shows   "R2 ≤ JF1rel R1 ∧ R3 ≤ JF2rel R1"
  apply (insert CIH1 CIH2)
  unfolding F1.in_rel F2.in_rel ex_simps(6)[symmetric] choice_iff
  apply (erule exE)+
  apply (rule conjI)

   apply (rule predicate2I)
   apply (rule iffD2[OF in_JF1rel])
   apply (rule exI conjI)+
    apply (rule CollectI)
    apply (rule rev_mp[OF conjunct1[OF J_rel_coind_ind]])
      apply assumption
     apply assumption
    apply (erule thin_rl)
    apply (erule thin_rl)
    apply (rule impI)
    apply (rule subsetI CollectI iffD2[OF case_prod_beta])+
    apply (drule bspec)
     apply assumption
    apply (erule allE mp conjE)+
    apply (erule conjI[OF _ refl])

   apply (rule conjI)
    apply (rule rev_mp[OF conjunct1[OF J_rel_coind_coind1]])
      apply assumption
     apply assumption
    apply (erule thin_rl)
    apply (erule thin_rl)
    apply (rule impI)
    apply (erule mp)
    apply (rule exI)
    apply (erule conjI[OF _ refl])

   apply (rule rev_mp[OF conjunct1[OF J_rel_coind_coind2]])
     apply assumption
    apply assumption
   apply (erule thin_rl)
   apply (erule thin_rl)
   apply (rule impI)
   apply (erule mp)
   apply (rule exI)
   apply (erule conjI[OF _ refl])

(**)

  apply (rule predicate2I)
  apply (rule iffD2[OF in_JF2rel])
  apply (rule exI conjI)+
   apply (rule rev_mp[OF conjunct2[OF J_rel_coind_ind]])
     apply assumption
    apply assumption
   apply (erule thin_rl)
   apply (erule thin_rl)
   apply (rule impI)
   apply (rule CollectI)
   apply (rule subsetI CollectI iffD2[OF case_prod_beta])+
   apply (drule bspec)
    apply assumption
   apply (erule allE mp conjE)+
   apply (erule conjI[OF _ refl])

  apply (rule conjI)
   apply (rule rev_mp[OF conjunct2[OF J_rel_coind_coind1]])
     apply assumption
    apply assumption
   apply (erule thin_rl)
   apply (erule thin_rl)
   apply (rule impI)
   apply (erule mp)
   apply (rule exI)
   apply (erule conjI[OF _ refl])

  apply (rule rev_mp[OF conjunct2[OF J_rel_coind_coind2]])
    apply assumption
   apply assumption
  apply (erule thin_rl)
  apply (erule thin_rl)
  apply (rule impI)
  apply (erule mp)
  apply (rule exI)
  apply (erule conjI[OF _ refl])
  done

lemma JF1rel_F1rel: "JF1rel R a b ⟷ F1rel R (JF1rel R) (JF2rel R) (dtor1 a) (dtor1 b)"
  apply (rule iffI)
   apply (drule iffD1[OF in_JF1rel])
   apply (erule exE conjE CollectE)+
   apply (rule iffD2[OF F1.in_rel])
   apply (rule exI)
   apply (rule conjI)
    apply (rule CollectI)
    apply (rule conjI)
     apply (rule ord_eq_le_trans)
      apply (rule F1.set_map(1))
     apply (rule ord_eq_le_trans)
      apply (rule trans[OF fun_cong[OF image_id] id_apply])
     apply (erule subset_trans[OF F1set1_incl_JF1set])

    apply (rule conjI)
     apply (rule ord_eq_le_trans)
      apply (rule F1.set_map(2))
     apply (rule image_subsetI)
     apply (rule CollectI)
     apply (rule case_prodI)
     apply (rule iffD2[OF in_JF1rel])
     apply (rule exI)
     apply (rule conjI)
      apply (rule CollectI)
      apply (erule subset_trans[OF F1set2_JF1set_incl_JF1set])
      apply assumption
     apply (rule conjI)
      apply (rule refl)
     apply (rule refl)

    apply (rule ord_eq_le_trans)
     apply (rule F1.set_map(3))
    apply (rule image_subsetI)
    apply (rule CollectI)
    apply (rule case_prodI)
    apply (rule iffD2[OF in_JF2rel])
    apply (rule exI)
    apply (rule conjI)
     apply (rule CollectI)
     apply (erule subset_trans[OF F1set3_JF2set_incl_JF1set])
     apply assumption
    apply (rule conjI)
     apply (rule refl)
    apply (rule refl)
   apply (rule conjI)

    apply (rule trans)
     apply (rule F1.map_comp)
    apply (rule trans)
     apply (rule F1.map_cong0)
       apply (rule fun_cong[OF o_id])
      apply (rule trans)
       apply (rule o_apply)
      apply (rule fst_conv)
     apply (rule trans)
      apply (rule o_apply)
     apply (rule fst_conv)
    apply (rule trans)
     apply (rule sym)
     apply (rule JF1map_simps)
    apply (rule iffD2[OF dtor1_diff])
    apply assumption

   apply (rule trans)
    apply (rule F1.map_comp)
   apply (rule trans)
    apply (rule F1.map_cong0)
      apply (rule fun_cong[OF o_id])
     apply (rule trans)
      apply (rule o_apply)
     apply (rule snd_conv)
    apply (rule trans)
     apply (rule o_apply)
    apply (rule snd_conv)
   apply (rule trans)
    apply (rule sym)
    apply (rule JF1map_simps)
   apply (rule iffD2[OF dtor1_diff])
   apply assumption

  apply (drule iffD1[OF F1.in_rel])
  apply (erule exE conjE CollectE)+
  apply (rule iffD2[OF in_JF1rel])
  apply (rule exI)
  apply (rule conjI)
   apply (rule CollectI)
   apply (rule ord_eq_le_trans)
    apply (rule JF1set_simps)
   apply (rule Un_least)
    apply (rule ord_eq_le_trans)
     apply (rule box_equals)
       apply (rule F1.set_map(1))
      apply (rule arg_cong[OF sym[OF dtor1_ctor1]])
     apply (rule trans[OF fun_cong[OF image_id] id_apply])
    apply assumption
   apply (rule Un_least)
    apply (rule ord_eq_le_trans)
     apply (rule SUP_cong[OF _ refl])
     apply (rule box_equals[OF _ _ refl])
      apply (rule F1.set_map(2))
     apply (rule arg_cong[OF sym[OF dtor1_ctor1]])
    apply (rule UN_least)
    apply (drule rev_subsetD)
     apply (erule image_mono)
    apply (erule imageE)
    apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
    apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
    apply hypsubst
    apply (drule iffD1[OF in_JF1rel])
    apply (drule someI_ex)
    apply (erule conjE)+
    apply (erule CollectE conjE)+
    apply assumption

   apply (rule ord_eq_le_trans)
    apply (rule trans[OF arg_cong[OF dtor1_ctor1]])
    apply (rule arg_cong[OF F1.set_map(3)])
   apply (rule UN_least)
   apply (drule rev_subsetD)
    apply (erule image_mono)
   apply (erule imageE)
   apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
   apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
   apply hypsubst
   apply (drule iffD1[OF in_JF2rel])
   apply (drule someI_ex)
   apply (erule exE conjE)+
   apply (erule CollectD)

  apply (rule conjI)

   apply (rule iffD1[OF dtor1_diff])
   apply (rule trans)
    apply (rule JF1map_simps)
   apply (rule box_equals)
     apply (rule F1.map_comp)
    apply (rule arg_cong[OF sym[OF dtor1_ctor1]])
   apply (rule trans)
    apply (rule F1.map_cong0)
      apply (rule fun_cong[OF o_id])
     apply (rule trans[OF o_apply])
     apply (drule rev_subsetD)
      apply assumption
     apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
     apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
     apply hypsubst
     apply (drule iffD1[OF in_JF1rel])
     apply (drule someI_ex)
     apply (erule conjE)+
     apply assumption
    apply (rule trans[OF o_apply])
    apply (drule rev_subsetD)
     apply assumption
    apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
    apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
    apply hypsubst
    apply (drule iffD1[OF in_JF2rel])
    apply (drule someI_ex)
    apply (erule conjE)+
    apply assumption
   apply assumption

  apply (rule iffD1[OF dtor1_diff])
  apply (rule trans)
   apply (rule JF1map_simps)
  apply (rule trans)
   apply (rule arg_cong[OF dtor1_ctor1])
  apply (rule trans)
   apply (rule F1.map_comp)
  apply (rule trans)
   apply (rule F1.map_cong0)
     apply (rule fun_cong[OF o_id])
    apply (rule trans[OF o_apply])
    apply (drule rev_subsetD)
     apply assumption
    apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
    apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
    apply hypsubst
    apply (drule iffD1[OF in_JF1rel])
    apply (drule someI_ex)
    apply (erule conjE)+
    apply assumption
   apply (rule trans[OF o_apply])
   apply (drule rev_subsetD)
    apply assumption
   apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
   apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
   apply hypsubst
   apply (drule iffD1[OF in_JF2rel])
   apply (drule someI_ex)
   apply (erule conjE)+
   apply assumption
  apply assumption
  done

lemma JF2rel_F2rel: "JF2rel R a b ⟷ F2rel R (JF1rel R) (JF2rel R) (dtor2 a) (dtor2 b)"
  apply (rule iffI)
   apply (drule iffD1[OF in_JF2rel])
   apply (erule exE conjE CollectE)+
   apply (rule iffD2[OF F2.in_rel])
   apply (rule exI)
   apply (rule conjI)
    apply (rule CollectI)
    apply (rule conjI)
     apply (rule ord_eq_le_trans)
      apply (rule F2.set_map(1))
     apply (rule ord_eq_le_trans)
      apply (rule trans[OF fun_cong[OF image_id] id_apply])
     apply (rule subset_trans)
      apply (rule F2set1_incl_JF2set)
     apply assumption

    apply (rule conjI)
     apply (rule ord_eq_le_trans)
      apply (rule F2.set_map(2))
     apply (rule image_subsetI)
     apply (rule CollectI)
     apply (rule case_prodI)
     apply (rule iffD2[OF in_JF1rel])
     apply (rule exI)
     apply (rule conjI)
      apply (rule CollectI)
      apply (rule subset_trans)
       apply (rule F2set2_JF1set_incl_JF2set)
       apply assumption
      apply assumption
     apply (rule conjI)
      apply (rule refl)
     apply (rule refl)

    apply (rule ord_eq_le_trans)
     apply (rule F2.set_map(3))
    apply (rule image_subsetI)
    apply (rule CollectI)
    apply (rule case_prodI)
    apply (rule iffD2[OF in_JF2rel])
    apply (rule exI)
    apply (rule conjI)
     apply (rule CollectI)
     apply (rule subset_trans)
      apply (rule F2set3_JF2set_incl_JF2set)
      apply assumption
     apply assumption
    apply (rule conjI)
     apply (rule refl)
    apply (rule refl)
   apply (rule conjI)

    apply (rule trans)
     apply (rule F2.map_comp)
    apply (rule trans)
     apply (rule F2.map_cong0)
       apply (rule fun_cong[OF o_id])
      apply (rule trans)
       apply (rule o_apply)
      apply (rule fst_conv)
     apply (rule trans)
      apply (rule o_apply)
     apply (rule fst_conv)
    apply (rule trans)
     apply (rule sym)
     apply (rule JF2map_simps)
    apply (rule iffD2)
     apply (rule dtor2_diff)
    apply assumption

   apply (rule trans)
    apply (rule F2.map_comp)
   apply (rule trans)
    apply (rule F2.map_cong0)
      apply (rule fun_cong[OF o_id])
     apply (rule trans)
      apply (rule o_apply)
     apply (rule snd_conv)
    apply (rule trans)
     apply (rule o_apply)
    apply (rule snd_conv)
   apply (rule trans)
    apply (rule sym)
    apply (rule JF2map_simps)
   apply (rule iffD2)
    apply (rule dtor2_diff)
   apply assumption

  apply (drule iffD1[OF F2.in_rel])
  apply (erule exE conjE CollectE)+
  apply (rule iffD2[OF in_JF2rel])
  apply (rule exI)
  apply (rule conjI)
   apply (rule CollectI)
   apply (rule ord_eq_le_trans)
    apply (rule JF2set_simps)
   apply (rule Un_least)
    apply (rule ord_eq_le_trans)
     apply (rule trans)
      apply (rule trans)
       apply (rule arg_cong[OF dtor2_ctor2])
      apply (rule F2.set_map(1))
     apply (rule trans[OF fun_cong[OF image_id] id_apply])
    apply assumption
   apply (rule Un_least)
    apply (rule ord_eq_le_trans)
     apply (rule trans[OF arg_cong[OF dtor2_ctor2]])
     apply (rule arg_cong[OF F2.set_map(2)])
    apply (rule UN_least)
    apply (drule rev_subsetD)
     apply (erule image_mono)
    apply (erule imageE)
    apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
    apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
    apply hypsubst
    apply (drule iffD1[OF in_JF1rel])
    apply (drule someI_ex)
    apply (erule conjE)+
    apply (erule CollectD)

   apply (rule ord_eq_le_trans)
    apply (rule trans[OF arg_cong[OF dtor2_ctor2]])
    apply (rule arg_cong[OF F2.set_map(3)])
   apply (rule UN_least)
   apply (drule rev_subsetD)
    apply (erule image_mono)
   apply (erule imageE)
   apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
   apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
   apply hypsubst
   apply (drule iffD1[OF in_JF2rel])
   apply (drule someI_ex)
   apply (erule exE conjE)+
   apply (erule CollectD)

  apply (rule conjI)

   apply (rule iffD1)
    apply (rule dtor2_diff)
   apply (rule trans)
    apply (rule JF2map_simps)
   apply (rule trans)
    apply (rule arg_cong[OF dtor2_ctor2])
   apply (rule trans)
    apply (rule F2.map_comp)
   apply (rule trans)
    apply (rule F2.map_cong0)
      apply (rule fun_cong[OF o_id])
     apply (rule trans[OF o_apply])
     apply (drule rev_subsetD)
      apply assumption
     apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
     apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
     apply hypsubst
     apply (drule iffD1[OF in_JF1rel])
     apply (drule someI_ex)
     apply (erule conjE)+
     apply assumption
    apply (rule trans[OF o_apply])
    apply (drule rev_subsetD)
     apply assumption
    apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
    apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
    apply hypsubst
    apply (drule iffD1[OF in_JF2rel])
    apply (drule someI_ex)
    apply (erule conjE)+
    apply assumption
   apply assumption

  apply (rule iffD1)
   apply (rule dtor2_diff)
  apply (rule trans)
   apply (rule JF2map_simps)
  apply (rule trans)
   apply (rule arg_cong[OF dtor2_ctor2])
  apply (rule trans)
   apply (rule F2.map_comp)
  apply (rule trans)
   apply (rule F2.map_cong0)
     apply (rule fun_cong[OF o_id])
    apply (rule trans[OF o_apply])
    apply (drule rev_subsetD)
     apply assumption
    apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
    apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
    apply hypsubst
    apply (drule iffD1[OF in_JF1rel])
    apply (drule someI_ex)
    apply (erule conjE)+
    apply assumption
   apply (rule trans[OF o_apply])
   apply (drule rev_subsetD)
    apply assumption
   apply (drule ssubst_mem[OF surjective_pairing[symmetric]])
   apply (erule CollectE case_prodE iffD1[OF prod.inject, elim_format] conjE)+
   apply hypsubst
   apply (drule iffD1[OF in_JF2rel])
   apply (drule someI_ex)
   apply (erule conjE)+
   apply assumption
  apply assumption
  done

lemma JFrel_Comp_le:
  "JF1rel R1 OO JF1rel R2 ≤ JF1rel (R1 OO R2) ∧ JF2rel R1 OO JF2rel R2 ≤ JF2rel (R1 OO R2)"
  apply (rule J_rel_coind[OF allI[OF allI[OF impI]] allI[OF allI[OF impI]]])
   apply (rule predicate2D[OF eq_refl[OF sym[OF F1.rel_compp]]])
   apply (erule relcomppE)
   apply (rule relcomppI)
    apply (erule iffD1[OF JF1rel_F1rel])
   apply (erule iffD1[OF JF1rel_F1rel])
  apply (rule predicate2D[OF eq_refl[OF sym[OF F2.rel_compp]]])
  apply (erule relcomppE)
  apply (rule relcomppI)
   apply (erule iffD1[OF JF2rel_F2rel])
  apply (erule iffD1[OF JF2rel_F2rel])
  done

context includes lifting_syntax
begin

lemma unfold_transfer:
  "((S ===> F1rel R S T) ===> (T ===> F2rel R S T) ===> S ===> JF1rel R) unfold1 unfold1 ∧
  ((S ===> F1rel R S T) ===> (T ===> F2rel R S T) ===> T ===> JF2rel R) unfold2 unfold2"
  unfolding rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]
  unfolding rel_fun_iff_geq_image2p
  apply (rule allI impI)+
  apply (rule J_rel_coind)
   apply (rule allI impI)+
   apply (erule image2pE)
   apply hypsubst
   apply (unfold unfold1 unfold2) [1]
   apply (rule rel_funD[OF rel_funD[OF rel_funD[OF rel_funD[OF F1.map_transfer]]]])
      apply (rule id_transfer)
     apply (rule rel_fun_image2p)
    apply (rule rel_fun_image2p)
   apply (erule predicate2D)
   apply (erule image2pI)

  apply (rule allI impI)+
  apply (erule image2pE)
  apply hypsubst
  apply (unfold unfold1 unfold2) [1]
  apply (rule rel_funD[OF rel_funD[OF rel_funD[OF rel_funD[OF F2.map_transfer]]]])
     apply (rule id_transfer)
    apply (rule rel_fun_image2p)
   apply (rule rel_fun_image2p)
  apply (erule predicate2D)
  apply (erule image2pI)
  done

end

ML ‹
 BNF_FP_Util.mk_xtor_co_iter_o_map_thms BNF_Util.Greatest_FP false 1 @{thm unfold_unique}
 @{thms JF1map JF2map} (map (BNF_Tactics.mk_pointfree2 @{context}) @{thms unfold1 unfold2})
 @{thms F1.map_comp0[symmetric] F2.map_comp0[symmetric]} @{thms F1.map_cong0 F2.map_cong0}
 ›

ML ‹
 BNF_FP_Util.mk_xtor_co_iter_o_map_thms BNF_Util.Greatest_FP true 1 @{thm corec_unique}
 @{thms JF1map JF2map} (map (BNF_Tactics.mk_pointfree2 @{context}) @{thms corec1 corec2})
 @{thms F1.map_comp0[symmetric] F2.map_comp0[symmetric]} @{thms F1.map_cong0 F2.map_cong0}
 ›

bnf "'a JF1"
  map: JF1map
  sets: JF1set
  bd: bd_F
  wits: JF1wit
  rel: JF1rel
            apply -
            apply (rule JF1map_id)
           apply (rule JF1map_comp)
          apply (erule JF1map_cong0[OF ballI])
         apply (rule JF1set_natural)
        apply (rule bd_F_card_order)
       apply (rule conjunct1[OF bd_F_Cinfinite])
      apply (rule bd_F_regularCard)
     apply (rule JF1set_bd)
    apply (rule conjunct1[OF JFrel_Comp_le])
   apply (rule JF1rel_def[unfolded OO_Grp_alt mem_Collect_eq])
  apply (erule JF1wit)
  done

bnf "'a JF2"
  map: JF2map
  sets: JF2set
  bd: bd_F
  wits: JF2wit
  rel: JF2rel
            apply -
            apply (rule JF2map_id)
           apply (rule JF2map_comp)
          apply (erule JF2map_cong0[OF ballI])
         apply (rule JF2set_natural)
        apply (rule bd_F_card_order)
       apply (rule conjunct1[OF bd_F_Cinfinite])
      apply (rule bd_F_regularCard)
     apply (rule JF2set_bd)
    apply (rule conjunct2[OF JFrel_Comp_le])
   apply (rule JF2rel_def[unfolded OO_Grp_alt mem_Collect_eq])
  apply (erule JF2wit)
  done

(*<*)
end
(*>*)