simplifications of internal codatatype construction

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 19 08:34:34 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 19 09:50:50 2014 +0100
@@ -982,7 +982,6 @@
        end;
 
     val sbdTs = replicate n sbdT;
-    val sum_sbd = Library.foldr1 (uncurry mk_csum) (replicate n sbd);
     val sum_sbdT = mk_sumTN sbdTs;
     val sum_sbd_listT = HOLogic.listT sum_sbdT;
     val sum_sbd_list_setT = HOLogic.mk_setT sum_sbd_listT;
@@ -1068,8 +1067,6 @@
     val isTree =
       let
         val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl);
-        val Field = mk_leq Kl (mk_Field (mk_clists sum_sbd));
-        val prefCl = mk_prefCl Kl;
 
         val tree = mk_Ball Kl (Term.absfree kl'
           (HOLogic.mk_conj
@@ -1078,12 +1075,8 @@
               mk_Ball Succ (Term.absfree k' (mk_isNode
                 (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i)))
             Succs ks kks kks'))));
-
-        val undef = list_all_free [kl] (HOLogic.mk_imp
-          (HOLogic.mk_not (HOLogic.mk_mem (kl, Kl)),
-          HOLogic.mk_eq (lab $ kl, mk_undefined sbdFT)));
       in
-        Library.foldr1 HOLogic.mk_conj [empty, Field, prefCl, tree, undef]
+        HOLogic.mk_conj (empty, tree)
       end;
 
     val carT_binds = mk_internal_bs carTN;
@@ -1164,7 +1157,6 @@
       thm OF [set_sbd, sbd_Card_order]) o drop m) set_sbdss;
 
     val to_sbd_inj_thmss = mk_to_sbd_thmss @{thm toCard_inj};
-    val to_sbd_thmss = mk_to_sbd_thmss @{thm toCard};
     val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard};
 
     val Lev_bind = mk_internal_b LevN;
@@ -1273,10 +1265,8 @@
           Term.absfree k' (mk_InN bdFTs
             (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i);
 
-        val Lab = Term.absfree kl' (mk_If
-          (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z))
-          (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z))
-          (mk_undefined sbdFT));
+        val Lab = Term.absfree kl'
+          (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z));
 
         val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
           (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
@@ -1305,24 +1295,6 @@
         Term.list_comb (Const (nth behs (i - 1), behT), ss)
       end;
 
-    val Lev_sbd_thms =
-      let
-        fun mk_conjunct i z = mk_leq (mk_Lev ss nat i $ z) (mk_Field (mk_clists sum_sbd));
-        val goal = list_all_free zs
-          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
-
-        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
-
-        val Lev_sbd = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_Lev_sbd_tac lthy cts Lev_0s Lev_Sucs to_sbd_thmss))
-          |> Thm.close_derivation);
-
-        val Lev_sbd' = mk_specN n Lev_sbd;
-      in
-        map (fn i => Lev_sbd' RS mk_conjunctN n i) ks
-      end;
-
     val (length_Lev_thms, length_Lev'_thms) =
       let
         fun mk_conjunct i z = HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
@@ -1352,26 +1324,6 @@
         (length_Levs, length_Levs')
       end;
 
-    val prefCl_Lev_thms =
-      let
-        fun mk_conjunct i z = HOLogic.mk_imp
-          (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), mk_prefixeq kl_copy kl),
-          HOLogic.mk_mem (kl_copy, mk_Lev ss (mk_size kl_copy) i $ z));
-        val goal = list_all_free (kl :: kl_copy :: zs)
-          (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
-
-        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
-
-        val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_prefCl_Lev_tac lthy cts Lev_0s Lev_Sucs)))
-          |> Thm.close_derivation;
-
-        val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev;
-      in
-        map (fn i => prefCl_Lev' RS mk_conjunctN n i RS mp) ks
-      end;
-
     val rv_last_thmss =
       let
         fun mk_conjunct i z i' z_copy = list_exists_free [z_copy]
@@ -1479,9 +1431,9 @@
           (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks))))
         (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
           beh_defs carT_defs strT_defs isNode_defs
-          to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
-          length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss set_Lev_thmsss
-          set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s map_arg_cong_thms)
+          to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss
+          length_Lev_thms length_Lev'_thms rv_last_thmss set_Lev_thmsss
+          set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s)
       |> Thm.close_derivation;
 
     val timer = time (timer "Behavioral morphism");

--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 19 08:34:34 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 19 09:50:50 2014 +0100
@@ -9,8 +9,6 @@
 
 signature BNF_GFP_TACTICS =
 sig
-  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list list ->
-    tactic
   val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic
   val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
@@ -54,8 +52,8 @@
   val mk_mor_UNIV_tac: thm list -> thm -> tactic
   val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
     thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
-    thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
-    thm list list list -> thm list list -> thm list -> thm list -> thm list -> tactic
+    thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
+    thm list list -> thm list -> thm list -> tactic
   val mk_mor_case_sum_tac: 'a list -> thm -> tactic
   val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
   val mk_mor_elim_tac: thm -> tactic
@@ -65,7 +63,6 @@
   val mk_mor_str_tac: 'a list -> thm -> tactic
   val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
     thm list -> tactic
-  val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
   val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
     thm list -> thm list -> thm -> thm list -> tactic
   val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
@@ -372,9 +369,7 @@
           rtac conjI,
           rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp,
             etac equalityD1, etac CollectD,
-          rtac conjI, etac @{thm Shift_clists},
-          rtac conjI, etac @{thm Shift_prefCl},
-          rtac conjI, rtac ballI,
+          rtac ballI,
             rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
             SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),
             etac bspec, etac @{thm ShiftD},
@@ -387,8 +382,6 @@
               CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
                 rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
                 rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
-          rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE],
-          etac @{thm not_in_Shift}, rtac trans, rtac (@{thm shift_def} RS fun_cong), atac,
           dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec,
           etac @{thm set_mp[OF equalityD1]}, atac,
           REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
@@ -403,28 +396,6 @@
     CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1
   end;
 
-fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
-  let
-    val n = length Lev_0s;
-    val ks = 1 upto n;
-  in
-    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
-      REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn Lev_0 =>
-        EVERY' (map rtac [ord_eq_le_trans, Lev_0, @{thm Nil_clists}])) Lev_0s,
-      REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn (Lev_Suc, to_sbds) =>
-        EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
-          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
-            (fn (i, to_sbd) => EVERY' [rtac subsetI,
-              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
-              rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
-              etac set_rev_mp, REPEAT_DETERM o etac allE,
-              etac (mk_conjunctN n i)])
-          (rev (ks ~~ to_sbds))])
-      (Lev_Sucs ~~ to_sbdss)] 1
-  end;
-
 fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
   let
     val n = length Lev_0s;
@@ -449,37 +420,6 @@
 fun mk_length_Lev'_tac length_Lev =
   EVERY' [ftac length_Lev, etac ssubst, atac] 1;
 
-fun mk_prefCl_Lev_tac ctxt cts Lev_0s Lev_Sucs =
-  let
-    val n = length Lev_0s;
-    val ks = n downto 1;
-  in
-    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
-      REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn Lev_0 =>
-        EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
-          etac @{thm singletonE}, hyp_subst_tac ctxt,
-          dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
-          hyp_subst_tac ctxt,
-          rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
-          rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
-      REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
-        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
-          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
-            (fn i =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
-              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac ctxt,
-              rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
-              rtac Lev_0, rtac @{thm singletonI},
-              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt,
-              rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
-              rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
-              rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
-              etac mp, etac conjI, atac]) ks])
-      (Lev_0s ~~ Lev_Sucs)] 1
-  end;
-
 fun mk_rv_last_tac cTs cts rv_Nils rv_Conss =
   let
     val n = length rv_Nils;
@@ -610,37 +550,28 @@
       ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
   end;
 
-fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
-  to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
-  prefCl_Levs rv_lastss set_Levsss set_image_Levsss set_map0ss
-  map_comp_ids map_cong0s map_arg_congs =
+fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss
+  from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss length_Levs length_Lev's rv_lastss set_Levsss
+  set_image_Levsss set_map0ss map_comp_ids map_cong0s =
   let
     val n = length beh_defs;
     val ks = 1 upto n;
 
-    fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
-      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s,
-        (set_Levss, set_image_Levss))))))))))) =
+    fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'),
+      (rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) =
       EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
         rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
         rtac conjI,
           rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp),
           rtac @{thm singletonI},
-        rtac conjI,
-          rtac @{thm UN_least}, rtac Lev_sbd,
-        rtac conjI,
-          rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
-          rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
-          etac @{thm prefixeq_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
-        rtac conjI,
+        (**)
           rtac ballI, etac @{thm UN_E}, rtac conjI,
           if n = 1 then K all_tac else rtac (mk_sumEN n),
           EVERY' (map5 (fn i => fn isNode_def => fn set_map0s => fn set_Levs => fn set_image_Levs =>
             EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
               rtac exI, rtac conjI,
-              (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
-              else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
-                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
+              if n = 1 then rtac refl
+              else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i),
               CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
                 EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -657,9 +588,8 @@
               REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
               rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
               rtac exI, rtac conjI,
-              (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
-              else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
-                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
+              if n = 1 then rtac refl
+              else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i),
               CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
                 EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -673,12 +603,8 @@
               (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
           (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
             (set_Levss ~~ set_image_Levss))))),
-        (**)
-          rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
-          etac notE, etac @{thm UN_I[OF UNIV_I]},
         (*root isNode*)
-          rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans),
-          rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI},
+          rtac (isNode_def RS ssubst), rtac exI, rtac conjI,
           CONVERSION (Conv.top_conv
             (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
           if n = 1 then rtac refl else rtac (mk_sum_caseN n i),
@@ -695,12 +621,9 @@
               rtac rv_Nil])
           (drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
 
-    fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
-      ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
+    fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)),
+      ((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
       EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
-        rtac (@{thm if_P} RS (if n = 1 then map_arg_cong else sum_weak_case_cong) RS trans),
-        rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
-        rtac Lev_0, rtac @{thm singletonI},
         CONVERSION (Conv.top_conv
           (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
         if n = 1 then K all_tac
@@ -726,37 +649,22 @@
             rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
             rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
-            rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
-            dtac asm_rl, dtac asm_rl, dtac asm_rl,
-            dtac (Lev_Suc RS equalityD1 RS set_mp),
-            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-                dtac list_inject_iffD1, etac conjE,
-                if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
-                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
-                  atac, atac, hyp_subst_tac ctxt, atac]
-                else etac (mk_InN_not_InM i' i'' RS notE)])
-            (rev ks),
-            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
-            REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
             CONVERSION (Conv.top_conv
               (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
             if n = 1 then K all_tac
             else rtac sum_weak_case_cong THEN' rtac (mk_sum_caseN n i' RS trans),
-            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
-            rtac refl])
+            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl])
         ks to_sbd_injs from_to_sbds)];
   in
     (rtac mor_cong THEN'
     EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN'
     stac mor_def THEN' rtac conjI THEN'
     CONJ_WRAP' fbetw_tac
-      (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
-        ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
-          (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))))) THEN'
+      (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~
+        (rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN'
     CONJ_WRAP' mor_tac
-      (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
-        ((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
+      (ks ~~ (strT_defs ~~ ((Lev_Sucs ~~ (rv_Nils ~~ rv_Conss)) ~~
+        ((map_comp_ids ~~ map_cong0s) ~~
           (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
   end;