diff --git a/examples/pseudo_bool/array/compilation/proofs/mccisProofScript.sml b/examples/pseudo_bool/array/compilation/proofs/mccisProofScript.sml
index ff255428b8..e4192e843d 100644
--- a/examples/pseudo_bool/array/compilation/proofs/mccisProofScript.sml
+++ b/examples/pseudo_bool/array/compilation/proofs/mccisProofScript.sml
@@ -77,7 +77,7 @@ Theorem machine_code_sound:
         get_graph_lad fs (EL 2 cl) = SOME gt ∧
         (
           (LENGTH cl = 3 ∧
-            out = concat (print_prob (mk_prob (full_encode_mccis gp gt)))) ∨
+            out = concat (print_annot_prob (mk_prob (full_encode_mccis gp gt)))) ∨
           (LENGTH cl = 4 ∧
             (
               out = mccis_eq_str (max_ccis_size gp gt) ∨
diff --git a/examples/pseudo_bool/array/compilation/proofs/mcisProofScript.sml b/examples/pseudo_bool/array/compilation/proofs/mcisProofScript.sml
index 495a7eeaeb..f33c2a8d83 100644
--- a/examples/pseudo_bool/array/compilation/proofs/mcisProofScript.sml
+++ b/examples/pseudo_bool/array/compilation/proofs/mcisProofScript.sml
@@ -77,7 +77,7 @@ Theorem machine_code_sound:
         get_graph_lad fs (EL 2 cl) = SOME gt ∧
         (
           (LENGTH cl = 3 ∧
-            out = concat (print_prob (mk_prob (full_encode_mcis gp gt)))) ∨
+            out = concat (print_annot_prob (mk_prob (full_encode_mcis gp gt)))) ∨
           (LENGTH cl = 4 ∧
             (
               out = mcis_eq_str (max_cis_size gp gt) ∨
diff --git a/examples/pseudo_bool/array/compilation/proofs/subgraph_isoProofScript.sml b/examples/pseudo_bool/array/compilation/proofs/subgraph_isoProofScript.sml
index a1edb7aa14..e7bca1cd0d 100644
--- a/examples/pseudo_bool/array/compilation/proofs/subgraph_isoProofScript.sml
+++ b/examples/pseudo_bool/array/compilation/proofs/subgraph_isoProofScript.sml
@@ -77,7 +77,7 @@ Theorem machine_code_sound:
         get_graph_lad fs (EL 2 cl) = SOME gt ∧
         (
           (LENGTH cl = 3 ∧
-            out = concat (print_prob (mk_prob (full_encode gp gt)))) ∨
+            out = concat (print_annot_prob (mk_prob (full_encode gp gt)))) ∨
           (LENGTH cl = 4 ∧
             (
               (out = «s VERIFIED NOT SUBGRAPH ISOMORPHIC\n» ∧
diff --git a/examples/pseudo_bool/array/mccisProgScript.sml b/examples/pseudo_bool/array/mccisProgScript.sml
index 5f685f8257..2daaea33d0 100644
--- a/examples/pseudo_bool/array/mccisProgScript.sml
+++ b/examples/pseudo_bool/array/mccisProgScript.sml
@@ -61,7 +61,10 @@ Theorem parse_and_enc_spec:
             (OPTION_TYPE (PAIR_TYPE
               (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE)))
             INT))
-            (LIST_TYPE (PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))
+            (LIST_TYPE
+              (PAIR_TYPE
+              (OPTION_TYPE STRING_TYPE)
+              (PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))))
             )) res v ∧
        case res of
         INL err =>
@@ -157,7 +160,8 @@ val res = translate map_concl_to_string_def;
 Definition mk_prob_def:
   mk_prob objf = (NONE,objf):mlstring list option #
     ((int # mlstring pbc$lit) list # int) option #
-    (pbop # (int # mlstring pbc$lit) list # int) list
+    (mlstring option #
+      (pbop # (int # mlstring pbc$lit) list # int)) list
 End
 
 val res = translate mk_prob_def;
@@ -167,10 +171,13 @@ val check_unsat_3 = (append_prog o process_topdecs) `
   case parse_and_enc f1 f2 of
     Inl err => TextIO.output TextIO.stdErr err
   | Inr (n,objf) =>
-    let val probt = default_prob in
+    let val probt = default_prob
+        val prob = mk_prob objf
+        val prob = strip_annot_prob prob
+    in
       (case
         map_concl_to_string n
-        (check_unsat_top_norm False (mk_prob objf) probt f3) of
+        (check_unsat_top_norm False prob probt f3) of
         Inl err => TextIO.output TextIO.stdErr err
       | Inr s => TextIO.print s)
     end`
@@ -223,11 +230,12 @@ Proof
   >-
     (xvar>>xsimpl)>>
   xlet_autop>>
+  xlet_autop>>
   xlet`POSTv v. STDIO fs * &BOOL F v`
   >-
     (xcon>>xsimpl)>>
   drule npbc_parseProgTheory.check_unsat_top_norm_spec>>
-  qpat_x_assum`prob_TYPE (mk_prob _) _`assume_tac>>
+  qpat_x_assum`prob_TYPE (strip_annot_prob _) _`assume_tac>>
   disch_then drule>>
   qpat_x_assum`prob_TYPE default_prob _`assume_tac>>
   disch_then drule>>
@@ -274,6 +282,8 @@ Proof
     qexists_tac`strlit ""`>>
     simp[STD_streams_stderr,add_stdo_nil]>>
     xsimpl>>
+    fs[oneline pb_parseTheory.strip_annot_prob_def]>>
+    every_case_tac>>gvs[]>>
     (drule_at Any) full_encode_mccis_sem_concl>>
     fs[]>>
     Cases_on`x`>> disch_then (drule_at Any)>>
@@ -281,7 +291,8 @@ Proof
     impl_tac>-
       fs[get_graph_lad_def,AllCaseEqs(),mk_prob_def]>>
     rw[]>>
-    qexists_tac`(q,r)`>>
+    rename1`(qq,rr)`>>
+    qexists_tac`(qq,rr)`>>
     simp[mccis_sem_def]>>
     metis_tac[])
 QED
@@ -294,7 +305,7 @@ Definition check_unsat_2_sem_def:
   case get_graph_lad fs f2 of
     NONE => out = strlit ""
   | SOME gtt =>
-    out = concat (print_prob
+    out = concat (print_annot_prob
       (mk_prob (full_encode_mccis gpp gtt)))
 End
 
@@ -303,7 +314,7 @@ val check_unsat_2 = (append_prog o process_topdecs) `
   case parse_and_enc f1 f2 of
     Inl err => TextIO.output TextIO.stdErr err
   | Inr (n,objf) =>
-    TextIO.print_list (print_prob (mk_prob objf))`
+    TextIO.print_list (print_annot_prob (mk_prob objf))`
 
 Theorem check_unsat_2_spec:
   STRING_TYPE f1 f1v ∧ validArg f1 ∧
diff --git a/examples/pseudo_bool/array/mcisProgScript.sml b/examples/pseudo_bool/array/mcisProgScript.sml
index c1b4c202bb..e026f72652 100644
--- a/examples/pseudo_bool/array/mcisProgScript.sml
+++ b/examples/pseudo_bool/array/mcisProgScript.sml
@@ -50,7 +50,10 @@ Theorem parse_and_enc_spec:
             (OPTION_TYPE (PAIR_TYPE
               (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE)))
             INT))
-            (LIST_TYPE (PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))
+            (LIST_TYPE
+              (PAIR_TYPE
+              (OPTION_TYPE STRING_TYPE)
+              (PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))))
             )) res v ∧
        case res of
         INL err =>
@@ -146,7 +149,8 @@ val res = translate map_concl_to_string_def;
 Definition mk_prob_def:
   mk_prob objf = (NONE,objf):mlstring list option #
     ((int # mlstring pbc$lit) list # int) option #
-    (pbop # (int # mlstring pbc$lit) list # int) list
+    (mlstring option #
+      (pbop # (int # mlstring pbc$lit) list # int)) list
 End
 
 val res = translate mk_prob_def;
@@ -156,10 +160,13 @@ val check_unsat_3 = (append_prog o process_topdecs) `
   case parse_and_enc f1 f2 of
     Inl err => TextIO.output TextIO.stdErr err
   | Inr (n,objf) =>
-    let val probt = default_prob in
+    let val probt = default_prob
+        val prob = mk_prob objf
+        val prob = strip_annot_prob prob
+    in
       (case
         map_concl_to_string n
-        (check_unsat_top_norm False (mk_prob objf) probt f3) of
+        (check_unsat_top_norm False prob probt f3) of
         Inl err => TextIO.output TextIO.stdErr err
       | Inr s => TextIO.print s)
     end`
@@ -212,11 +219,12 @@ Proof
   >-
     (xvar>>xsimpl)>>
   xlet_autop>>
+  xlet_autop>>
   xlet`POSTv v. STDIO fs * &BOOL F v`
   >-
     (xcon>>xsimpl)>>
   drule npbc_parseProgTheory.check_unsat_top_norm_spec>>
-  qpat_x_assum`prob_TYPE (mk_prob _) _`assume_tac>>
+  qpat_x_assum`prob_TYPE (strip_annot_prob _) _`assume_tac>>
   disch_then drule>>
   qpat_x_assum`prob_TYPE default_prob _`assume_tac>>
   disch_then drule>>
@@ -263,6 +271,8 @@ Proof
     qexists_tac`strlit ""`>>
     rw[]>>simp[STD_streams_stderr,add_stdo_nil]>>
     xsimpl>>
+    fs[oneline pb_parseTheory.strip_annot_prob_def]>>
+    every_case_tac>>gvs[]>>
     (drule_at Any) full_encode_mcis_sem_concl>>
     fs[]>>
     Cases_on`x`>> disch_then (drule_at Any)>>
@@ -270,7 +280,8 @@ Proof
     impl_tac>-
       fs[get_graph_lad_def,AllCaseEqs(),mk_prob_def]>>
     rw[]>>
-    qexists_tac`(q,r)`>>
+    rename1`(qq,rr)`>>
+    qexists_tac`(qq,rr)`>>
     simp[mcis_sem_def]>>
     metis_tac[])
 QED
@@ -283,7 +294,7 @@ Definition check_unsat_2_sem_def:
   case get_graph_lad fs f2 of
     NONE => out = strlit ""
   | SOME gtt =>
-    out = concat (print_prob
+    out = concat (print_annot_prob
       (mk_prob (full_encode_mcis gpp gtt)))
 End
 
@@ -292,7 +303,7 @@ val check_unsat_2 = (append_prog o process_topdecs) `
   case parse_and_enc f1 f2 of
     Inl err => TextIO.output TextIO.stdErr err
   | Inr (n,objf) =>
-    TextIO.print_list (print_prob (mk_prob objf))`
+    TextIO.print_list (print_annot_prob (mk_prob objf))`
 
 Theorem check_unsat_2_spec:
   STRING_TYPE f1 f1v ∧ validArg f1 ∧
diff --git a/examples/pseudo_bool/array/subgraph_isoProgScript.sml b/examples/pseudo_bool/array/subgraph_isoProgScript.sml
index 691992a0b3..069c34a915 100644
--- a/examples/pseudo_bool/array/subgraph_isoProgScript.sml
+++ b/examples/pseudo_bool/array/subgraph_isoProgScript.sml
@@ -45,8 +45,10 @@ Theorem parse_and_enc_spec:
     & ∃res.
      SUM_TYPE STRING_TYPE
        (LIST_TYPE
-       (PAIR_TYPE PBC_PBOP_TYPE
-          (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))) res v ∧
+        (PAIR_TYPE
+        (OPTION_TYPE STRING_TYPE)
+         (PAIR_TYPE PBC_PBOP_TYPE
+            (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))) res v ∧
       case res of
         INL err =>
         get_graph_lad fs f1 = NONE ∨ get_graph_lad fs f2 = NONE
@@ -110,7 +112,8 @@ val res = translate (res_to_string_def |> SIMP_RULE std_ss [UNSAT_string_def,SAT
 Definition mk_prob_def:
   mk_prob fml = (NONE,NONE,fml):mlstring list option #
     ((int # mlstring pbc$lit) list # int) option #
-    (pbop # (int # mlstring pbc$lit) list # int) list
+    (mlstring option #
+      (pbop # (int # mlstring pbc$lit) list # int)) list
 End
 
 val res = translate mk_prob_def;
@@ -120,9 +123,11 @@ val check_unsat_3 = (append_prog o process_topdecs) `
   case parse_and_enc f1 f2 of
     Inl err => TextIO.output TextIO.stdErr err
   | Inr fml =>
-    let val probt = default_prob in
+    let val probt = default_prob
+        val prob = mk_prob fml
+        val prob = strip_annot_prob prob in
     (case
-      res_to_string (check_unsat_top_norm False (mk_prob fml) probt f3) of
+      res_to_string (check_unsat_top_norm False prob probt f3) of
       Inl err => TextIO.output TextIO.stdErr err
     | Inr s => TextIO.print s)
     end`
@@ -174,6 +179,7 @@ Proof
   >-
     (xvar>>xsimpl)>>
   xlet_autop>>
+  xlet_autop>>
   xlet`POSTv v. STDIO fs * &BOOL F v`
   >-
     (xcon>>xsimpl)>>
@@ -225,6 +231,7 @@ Proof
     qexists_tac`strlit ""`>>
     simp[STD_streams_stderr,add_stdo_nil]>>
     xsimpl>>
+    fs[pb_parseTheory.strip_annot_prob_def]>>
     (drule_at Any) full_encode_sem_concl>>
     fs[]>>
     impl_tac >-
@@ -239,6 +246,7 @@ Proof
     qexists_tac`strlit ""`>>
     simp[STD_streams_stderr,add_stdo_nil]>>
     xsimpl>>
+    fs[pb_parseTheory.strip_annot_prob_def]>>
     (drule_at Any) full_encode_sem_concl>>
     fs[]>>
     impl_tac >-
@@ -264,7 +272,7 @@ Definition check_unsat_2_sem_def:
   case get_graph_lad fs f2 of
     NONE => out = strlit ""
   | SOME gtt =>
-    out = concat (print_prob (mk_prob (full_encode gpp gtt)))
+    out = concat (print_annot_prob (mk_prob (full_encode gpp gtt)))
 End
 
 val check_unsat_2 = (append_prog o process_topdecs) `
@@ -272,7 +280,7 @@ val check_unsat_2 = (append_prog o process_topdecs) `
   case parse_and_enc f1 f2 of
     Inl err => TextIO.output TextIO.stdErr err
   | Inr fml =>
-    TextIO.print_list (print_prob (mk_prob fml))`
+    TextIO.print_list (print_annot_prob (mk_prob fml))`
 
 Theorem check_unsat_2_spec:
   STRING_TYPE f1 f1v ∧ validArg f1 ∧
diff --git a/examples/pseudo_bool/graph_encoding/mcisScript.sml b/examples/pseudo_bool/graph_encoding/mcisScript.sml
index bf0467b65c..4ae7ec3b38 100644
--- a/examples/pseudo_bool/graph_encoding/mcisScript.sml
+++ b/examples/pseudo_bool/graph_encoding/mcisScript.sml
@@ -114,24 +114,36 @@ End
 
 (* For each a in vp, either a is unassigned or a is assigned to exactly one vertex
   v in vt *)
-Definition has_mapping_def:
-  has_mapping a vt =
-  (Equal,
+Definition has_mapping_al1_def:
+  has_mapping_al1 (a:num) vt =
+  ((strlit"al1" ^ toString a)
+  ,(GreaterEqual,
     (1, Pos (Unmapped a)) ::
     GENLIST (λv. (1, Pos (Mapped a v))) vt,
-    1): enc pbc
+    1): enc pbc)
+End
+
+Definition has_mapping_am1_def:
+  has_mapping_am1 (a:num) vt =
+  ((strlit"am1" ^ toString a)
+  ,(LessEqual,
+    (1, Pos (Unmapped a)) ::
+    GENLIST (λv. (1, Pos (Mapped a v))) vt,
+    1): enc pbc)
 End
 
 Definition all_has_mapping_def:
   all_has_mapping vp vt =
-  GENLIST (λa. has_mapping a vt) vp
+  GENLIST (λa. has_mapping_al1 a vt) vp ++
+  GENLIST (λa. has_mapping_am1 a vt) vp
 End
 
 Definition one_one_def:
   one_one u vp =
-  (GreaterEqual,
+  ((strlit"inj" ^ toString u)
+  ,(GreaterEqual,
     (GENLIST (λb. (1, Neg (Mapped b u))) vp),
-    (&vp-1)): enc pbc
+    (&vp-1)): enc pbc)
 End
 
 Definition all_one_one_def:
@@ -142,22 +154,26 @@ End
 Definition edge_map_def:
   edge_map (a,b) u et =
   if a = b then [] else
-  [(GreaterEqual,
+  [
+  (concat [strlit"adj"; toString a; strlit"_"; toString u; strlit"_"; toString b]
+  ,(GreaterEqual,
     (1,Neg (Mapped a u)) ::
     (1,Pos (Unmapped b)) ::
     MAP (λv. (1,Pos (Mapped b v))) (neighbours et u),
-    1):enc pbc]
+    1):enc pbc)]
 End
 
 Definition not_edge_map_def:
   not_edge_map (a,b) u vt et =
   if a = b then []
   else
-  [(GreaterEqual,
+  [
+  (concat [strlit"adj"; toString a; strlit"_"; toString u; strlit"_"; toString b]
+  ,(GreaterEqual,
     (1,Neg (Mapped a u)) ::
     (1,Pos (Unmapped b)) ::
     MAP (λv. (1,Pos (Mapped b v))) (not_neighbours (vt,et) u),
-    1):enc pbc]
+    1):enc pbc)]
 End
 
 Definition all_full_edge_map_def:
@@ -166,7 +182,9 @@ Definition all_full_edge_map_def:
     FLAT (GENLIST (λa.
       (* Check that a,u have same self-loop *)
       if is_edge ep a a ⇎ is_edge et u u
-      then [(GreaterEqual, [(1,Neg (Mapped a u))], 1):enc pbc]
+      then [
+        (concat [strlit"adj"; toString a; strlit"_"; toString u; strlit"_SELF"],
+        (GreaterEqual, [(1,Neg (Mapped a u))], 1):enc pbc)]
       else
         FLAT (MAP (λb. edge_map (a,b) u et) (neighbours ep a)) ++
         FLAT (MAP (λb. not_edge_map (a,b) u vt et) (not_neighbours (vp,ep) a) )) vp)) vt)
@@ -476,7 +494,7 @@ Theorem encode_base_correct:
       injective_partial_map f vs (vp,ep) (vt,et) ∧
       CARD vs = k) ⇔
     (∃w.
-      satisfies w (set constraints) ∧
+      satisfies w (set (MAP SND constraints)) ∧
       eval_obj (unmapped_obj vp) w = &vp - &k)
   )
 Proof
@@ -492,21 +510,22 @@ Proof
     rw[encode_base_def]
     >- (
       rename1`all_has_mapping`>>
-      simp[all_has_mapping_def,satisfies_def,MEM_GENLIST,has_mapping_def]>>
-      rw[]>>
-      simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
-      simp[iSUM_def]>>
-      Cases_on`a ∈ vs`>>simp[]
-      >- ( (* a ∈ vs *)
-        DEP_REWRITE_TAC[iSUM_eq_1]>>
+      simp[all_has_mapping_def,satisfies_def,MEM_GENLIST,MEM_MAP]>>
+      `∀a. a < vp ∧ a ∈ vs ⇒
+        iSUM (GENLIST (λv. b2i (f a = v)) vt) = 1` by (
+        rw[]>>
+        DEP_REWRITE_TAC[iSUM_eq_1,eval_lin_term_def]>>
         CONJ_TAC>-
           (simp[MEM_GENLIST]>>metis_tac[])>>
         qexists_tac`f a`>>
-        CONJ_ASM1_TAC>>fs[EL_GENLIST,INJ_DEF]) >>
-      simp[iSUM_GENLIST_const])
+        CONJ_ASM1_TAC>>fs[EL_GENLIST,INJ_DEF])>>
+      rw[]>>
+      simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def,
+        has_mapping_al1_def,has_mapping_am1_def]>>
+      Cases_on`a ∈ vs`>>simp[iSUM_def,iSUM_GENLIST_const])
     >- (
       rename1`all_one_one`>>
-      simp[all_one_one_def,satisfies_def,MEM_GENLIST,one_one_def]>>
+      simp[all_one_one_def,satisfies_def,MEM_GENLIST,one_one_def,MEM_MAP,PULL_EXISTS]>>
       rw[]>>
       simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
       fs[INJ_DEF]>>
@@ -628,11 +647,16 @@ Proof
   `∀n. n < vp ∧ ¬w (Unmapped n) ⇒
    ∃m. m < vt ∧ w (Mapped n m) ∧
    ∀m'. m' < vt ∧ w (Mapped n m') ⇔ m = m'` by (
-     fs[all_has_mapping_def,MEM_GENLIST,has_mapping_def,PULL_EXISTS]>>
+     fs[all_has_mapping_def,MEM_GENLIST,has_mapping_al1_def,
+      has_mapping_am1_def,PULL_EXISTS,MEM_MAP,PULL_EXISTS,SF DNF_ss]>>
      rw[]>>
      first_x_assum drule>>
+     first_x_assum drule>>
      simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
      simp[iSUM_def]>>
+     rw[]>>
+     `iSUM (GENLIST (λv. b2i (w (Mapped n v))) vt) = 1` by intLib.ARITH_TAC>>
+     pop_assum mp_tac>>
      DEP_REWRITE_TAC[iSUM_eq_1]>>
      CONJ_TAC>-
        (simp[MEM_GENLIST]>>metis_tac[])>>
@@ -649,7 +673,7 @@ Proof
     >- (
       first_x_assum drule>>strip_tac>>
       rfs[])>>
-    fs[all_one_one_def,MEM_GENLIST,PULL_EXISTS,one_one_def]>>
+    fs[all_one_one_def,MEM_GENLIST,PULL_EXISTS,one_one_def,MEM_MAP]>>
     res_tac>>
     gvs[]>>
     last_x_assum drule>>
@@ -1303,8 +1327,8 @@ End
 
 Definition encode_def:
   encode (vp,ep) (vt,et) =
-  encode_base (vp,ep) (vt,et) ++
-  encode_connected (vp,ep) vt
+  MAP (SOME ## I) (encode_base (vp,ep) (vt,et)) ++
+  MAP (λc. (NONE,c)) (encode_connected (vp,ep) vt)
 End
 
 Theorem walk_k_free:
@@ -1468,7 +1492,7 @@ Theorem encode_correct:
       injective_partial_map f vs (vp,ep) (vt,et) ∧
       connected_subgraph vs ep ∧
       CARD vs = k) ⇔
-    (∃w. satisfies w (set constraints) ∧
+    (∃w. satisfies w (set (MAP SND constraints)) ∧
       eval_obj (unmapped_obj vp) w = &vp - &k)
   )
 Proof
@@ -1488,21 +1512,22 @@ Proof
     rw[]
     >- (
       rename1`all_has_mapping`>>
-      simp[all_has_mapping_def,satisfies_def,MEM_GENLIST,has_mapping_def]>>
-      rw[]>>
-      simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
-      simp[iSUM_def]>>
-      Cases_on`a ∈ vs`>>simp[]
-      >- ( (* a ∈ vs *)
-        DEP_REWRITE_TAC[iSUM_eq_1]>>
+      simp[all_has_mapping_def,satisfies_def,MEM_GENLIST,MEM_MAP]>>
+      `∀a. a < vp ∧ a ∈ vs ⇒
+        iSUM (GENLIST (λv. b2i (f a = v)) vt) = 1` by (
+        rw[]>>
+        DEP_REWRITE_TAC[iSUM_eq_1,eval_lin_term_def]>>
         CONJ_TAC>-
           (simp[MEM_GENLIST]>>metis_tac[])>>
         qexists_tac`f a`>>
-        CONJ_ASM1_TAC>>fs[EL_GENLIST,INJ_DEF]) >>
-      simp[iSUM_GENLIST_const])
+        CONJ_ASM1_TAC>>fs[EL_GENLIST,INJ_DEF])>>
+      rw[]>>
+      simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def,
+        has_mapping_al1_def,has_mapping_am1_def]>>
+      Cases_on`a ∈ vs`>>simp[iSUM_def,iSUM_GENLIST_const])
     >- (
       rename1`all_one_one`>>
-      simp[all_one_one_def,satisfies_def,MEM_GENLIST,one_one_def]>>
+      simp[all_one_one_def,satisfies_def,MEM_GENLIST,one_one_def,MEM_MAP,PULL_EXISTS]>>
       rw[]>>
       simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
       fs[INJ_DEF]>>
@@ -1597,8 +1622,10 @@ Proof
         simp[]))
     >- (
       (* connectedness *)
-      rw[encode_connected_def]>>
-      simp[satisfies_def,MEM_FLAT,MEM_GENLIST,PULL_EXISTS,satisfies_pbc_def,eval_lin_term_def]>>
+      reverse(rw[encode_connected_def])>>
+      simp[satisfies_def,MEM_FLAT,MEM_GENLIST,PULL_EXISTS,satisfies_pbc_def,
+        eval_lin_term_def,MEM_MAP]
+      >- fs[satisfies_def]>>
       rw[]>>
       simp[satisfies_pbc_def,eval_lin_term_def]>>
       reverse (Cases_on`f' ∈ vs`)>>simp[iSUM_def]
@@ -1670,7 +1697,7 @@ Proof
     >- (
       fs[]>>
       simp[connected_subgraph_def])>>
-    fs[SF DNF_ss,MEM_FLAT,MEM_GENLIST,PULL_EXISTS,satisfies_pbc_def,eval_lin_term_def]>>
+    fs[SF DNF_ss,MEM_FLAT,MEM_GENLIST,PULL_EXISTS,satisfies_pbc_def,eval_lin_term_def,MEM_MAP]>>
     rw[connected_subgraph_def,Abbr`dom`]>>
     match_mp_tac is_walk_is_connected>>
     qpat_x_assum`good_graph (vp,ep)` assume_tac>>
@@ -1703,11 +1730,16 @@ Proof
   `∀n. n < vp ∧ ¬w (Unmapped n) ⇒
    ∃m. m < vt ∧ w (Mapped n m) ∧
    ∀m'. m' < vt ∧ w (Mapped n m') ⇔ m = m'` by (
-     fs[all_has_mapping_def,MEM_GENLIST,has_mapping_def,PULL_EXISTS]>>
+     fs[all_has_mapping_def,MEM_GENLIST,has_mapping_al1_def,
+      has_mapping_am1_def,PULL_EXISTS,MEM_MAP,PULL_EXISTS,SF DNF_ss]>>
      rw[]>>
      first_x_assum drule>>
+     first_x_assum drule>>
      simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
      simp[iSUM_def]>>
+     rw[]>>
+     `iSUM (GENLIST (λv. b2i (w (Mapped n v))) vt) = 1` by intLib.ARITH_TAC>>
+     pop_assum mp_tac>>
      DEP_REWRITE_TAC[iSUM_eq_1]>>
      CONJ_TAC>-
        (simp[MEM_GENLIST]>>metis_tac[])>>
@@ -1724,7 +1756,7 @@ Proof
     >- (
       first_x_assum drule>>strip_tac>>
       rfs[])>>
-    fs[all_one_one_def,MEM_GENLIST,PULL_EXISTS,one_one_def]>>
+    fs[all_one_one_def,MEM_GENLIST,PULL_EXISTS,one_one_def,MEM_MAP]>>
     res_tac>>
     gvs[]>>
     last_x_assum drule>>
@@ -1866,7 +1898,7 @@ Definition full_encode_mccis_def:
   full_encode_mccis gp gt =
   (map_obj enc_string
     (unmapped_obj (FST gp)),
-  MAP (map_pbc enc_string) (encode gp gt))
+  MAP (I ## map_pbc enc_string) (encode gp gt))
 End
 
 (* Convert minimization to maximization *)
@@ -1951,7 +1983,7 @@ Theorem full_encode_mccis_sem_concl:
   good_graph gp ∧
   good_graph gt ∧
   full_encode_mccis gp gt = (obj,pbf) ∧
-  sem_concl (set pbf) obj concl ∧
+  sem_concl (set (MAP SND pbf)) obj concl ∧
   conv_concl (FST gp) concl = SOME (lbg, ubg) ⇒
   (lbg = ubg ⇒ max_ccis_size gp gt = lbg) ∧
   (∀vs. is_ccis vs gp gt ⇒ CARD vs ≤ ubg) ∧
@@ -1960,7 +1992,8 @@ Proof
   strip_tac>>
   gvs[full_encode_mccis_def]>>
   qpat_x_assum`sem_concl _ _ _` mp_tac>>
-  simp[LIST_TO_SET_MAP]>>
+  simp[LIST_TO_SET_MAP,IMAGE_IMAGE]>>
+  simp[Once (GSYM IMAGE_IMAGE)]>>
   DEP_REWRITE_TAC[GSYM concl_INJ_iff]>>
   CONJ_TAC >- (
     assume_tac enc_string_INJ>>
@@ -1997,7 +2030,7 @@ Proof
     metis_tac[])>>
   rw[]
   >- ( (* Lower bound optimization *)
-    Cases_on`lbi`>>fs[unsatisfiable_def,satisfiable_def]
+    Cases_on`lbi`>>fs[unsatisfiable_def,satisfiable_def,LIST_TO_SET_MAP]
     >- (
       (* the formula is always satisfiable, so INF lower bound
          is impossible *)
@@ -2011,7 +2044,7 @@ Proof
     intLib.ARITH_TAC)>>
   (* Upper bound optimization *)
   Cases_on`ubi`>>
-  fs[SF DNF_ss,EQ_IMP_THM,is_ccis_def,is_cis_def]
+  fs[SF DNF_ss,EQ_IMP_THM,is_ccis_def,is_cis_def,LIST_TO_SET_MAP]
   >-
     metis_tac[injective_partial_map_exists,SND]>>
   `eval_obj (unmapped_obj q) w ≥ 0` by
@@ -2034,14 +2067,14 @@ Definition full_encode_mcis_def:
   full_encode_mcis gp gt =
   (map_obj enc_string
     (unmapped_obj (FST gp)),
-  MAP (map_pbc enc_string) (encode_base gp gt))
+  MAP (SOME ## map_pbc enc_string) (encode_base gp gt))
 End
 
 Theorem full_encode_mcis_sem_concl:
   good_graph gp ∧
   good_graph gt ∧
   full_encode_mcis gp gt = (obj,pbf) ∧
-  sem_concl (set pbf) obj concl ∧
+  sem_concl (set (MAP SND pbf)) obj concl ∧
   conv_concl (FST gp) concl = SOME (lbg, ubg) ⇒
   (lbg = ubg ⇒ max_cis_size gp gt = lbg) ∧
   (∀vs. is_cis vs gp gt ⇒ CARD vs ≤ ubg) ∧
@@ -2050,7 +2083,8 @@ Proof
   strip_tac>>
   gvs[full_encode_mcis_def]>>
   qpat_x_assum`sem_concl _ _ _` mp_tac>>
-  simp[LIST_TO_SET_MAP]>>
+  simp[LIST_TO_SET_MAP,IMAGE_IMAGE]>>
+  simp[Once (GSYM IMAGE_IMAGE)]>>
   DEP_REWRITE_TAC[GSYM concl_INJ_iff]>>
   CONJ_TAC >- (
     assume_tac enc_string_INJ>>
@@ -2086,7 +2120,8 @@ Proof
     metis_tac[])>>
   rw[]
   >- ( (* Lower bound optimization *)
-    Cases_on`lbi`>>fs[unsatisfiable_def,satisfiable_def,is_cis_def]
+    Cases_on`lbi`>>
+    fs[unsatisfiable_def,satisfiable_def,is_cis_def,LIST_TO_SET_MAP]
     >- (
       (* the formula is always satisfiable, so INF lower bound
          is impossible *)
@@ -2099,7 +2134,7 @@ Proof
     intLib.ARITH_TAC)>>
   (* Upper bound optimization *)
   Cases_on`ubi`>>
-  fs[SF DNF_ss,EQ_IMP_THM,is_cis_def]
+  fs[SF DNF_ss,EQ_IMP_THM,is_cis_def,LIST_TO_SET_MAP]
   >-
     metis_tac[injective_partial_map_exists]>>
   `eval_obj (unmapped_obj q) w ≥ 0` by
@@ -2120,8 +2155,10 @@ QED
 Theorem full_encode_mcis_eq =
   full_encode_mcis_def
   |> SIMP_RULE (srw_ss()) [FORALL_PROD,encode_base_def]
-  |> SIMP_RULE (srw_ss()) [all_has_mapping_def,all_one_one_def,all_full_edge_map_def,has_mapping_def,one_one_def,edge_map_def,not_edge_map_def]
-  |> SIMP_RULE (srw_ss()) [MAP_FLAT,MAP_GENLIST,MAP_APPEND,o_DEF,MAP_MAP_o,pbc_ge_def,map_pbc_def,FLAT_FLAT,FLAT_MAP_SING,map_lit_def,MAP_if]
+  |> SIMP_RULE (srw_ss()) [all_has_mapping_def,all_one_one_def,all_full_edge_map_def,
+    has_mapping_al1_def,has_mapping_am1_def,one_one_def,edge_map_def,not_edge_map_def]
+  |> SIMP_RULE (srw_ss()) [MAP_FLAT,MAP_GENLIST,MAP_APPEND,o_DEF,MAP_MAP_o,pbc_ge_def,
+    map_pbc_def,FLAT_FLAT,FLAT_MAP_SING,map_lit_def,MAP_if]
   |> SIMP_RULE (srw_ss()) [FLAT_GENLIST_FOLDN,FOLDN_APPEND,FOLDN_APPEND_op]
   |> PURE_ONCE_REWRITE_RULE [APPEND_OP_DEF]
   |> SIMP_RULE (srw_ss()) [];
@@ -2176,9 +2213,10 @@ Theorem walk_k_eq =
   |> SIMP_RULE (srw_ss()) [if_APPEND];
 
 val enc_encode_connected =
-  ``MAP (map_pbc enc_string) (encode_connected (p_1,p_2) vt)``
+  ``MAP (\c. (NONE:mlstring option,(map_pbc enc_string c))) (encode_connected (p_1,p_2) vt)``
   |> SIMP_CONV (srw_ss()) [encode_connected_thm]
-  |> SIMP_RULE (srw_ss()) [MAP_FLAT,MAP_GENLIST,MAP_APPEND,o_DEF,MAP_MAP_o,pbc_ge_def,map_pbc_def,FLAT_FLAT,FLAT_MAP_SING,map_lit_def,LET_DEF,MAP_if]
+  |> SIMP_RULE (srw_ss()) [MAP_FLAT,MAP_GENLIST,MAP_APPEND,o_DEF,MAP_MAP_o,
+    pbc_ge_def,map_pbc_def,FLAT_FLAT,FLAT_MAP_SING,map_lit_def,LET_DEF,MAP_if]
   |> SIMP_RULE (srw_ss()) [FLAT_GENLIST_FOLDN]
   |> PURE_REWRITE_RULE[GSYM APPEND_ASSOC]
   |> SIMP_RULE std_ss [FOLDN_APPEND]
@@ -2188,8 +2226,10 @@ val enc_encode_connected =
 Theorem full_encode_mccis_eq =
   full_encode_mccis_def
   |> SIMP_RULE (srw_ss()) [FORALL_PROD,encode_def,encode_base_def]
-  |> SIMP_RULE (srw_ss()) [all_has_mapping_def,all_one_one_def,all_full_edge_map_def,has_mapping_def,one_one_def,edge_map_def,not_edge_map_def]
-  |> SIMP_RULE (srw_ss()) [MAP_FLAT,MAP_GENLIST,MAP_APPEND,o_DEF,MAP_MAP_o,pbc_ge_def,map_pbc_def,FLAT_FLAT,FLAT_MAP_SING,map_lit_def,LET_DEF,MAP_if]
+  |> SIMP_RULE (srw_ss()) [all_has_mapping_def,all_one_one_def,all_full_edge_map_def,
+    has_mapping_al1_def,has_mapping_am1_def,one_one_def,edge_map_def,not_edge_map_def]
+  |> SIMP_RULE (srw_ss()) [MAP_FLAT,MAP_GENLIST,MAP_APPEND,o_DEF,MAP_MAP_o,pbc_ge_def,
+    map_pbc_def,FLAT_FLAT,FLAT_MAP_SING,map_lit_def,LET_DEF,MAP_if]
   |> SIMP_RULE (srw_ss()) [FLAT_GENLIST_FOLDN]
   |> PURE_REWRITE_RULE[GSYM APPEND_ASSOC]
   |> SIMP_RULE std_ss [FOLDN_APPEND]
diff --git a/examples/pseudo_bool/graph_encoding/subgraph_isoScript.sml b/examples/pseudo_bool/graph_encoding/subgraph_isoScript.sml
index d0fd179cfb..21b6edcd67 100644
--- a/examples/pseudo_bool/graph_encoding/subgraph_isoScript.sml
+++ b/examples/pseudo_bool/graph_encoding/subgraph_isoScript.sml
@@ -18,26 +18,38 @@ End
 Type map_var = ``:num # num``
 
 (* For a in vp, vp is mapped to exactly 1 target in vt *)
-Definition has_mapping_def:
-  has_mapping (a:num) vt =
-  (Equal, (GENLIST (λv. (1, Pos (a,v))) vt), 1):map_var pbc
+Definition has_mapping_al1_def:
+  has_mapping_al1 (a:num) vt =
+  ((strlit"al1" ^ toString a)
+  ,(GreaterEqual, (GENLIST (λv. (1, Pos (a,v))) vt), 1):map_var pbc)
+End
+
+Definition has_mapping_am1_def:
+  has_mapping_am1 (a:num) vt =
+  ((strlit"am1" ^ toString a)
+  ,(LessEqual, (GENLIST (λv. (1, Pos (a,v))) vt), 1):map_var pbc)
 End
 
 Definition one_one_def:
   one_one u vp =
-  (GreaterEqual, GENLIST (λb. (1, Neg (b,u))) vp, &vp-1): map_var pbc
+  ((strlit"inj" ^ toString u)
+  ,(GreaterEqual, GENLIST (λb. (1, Neg (b,u))) vp, &vp-1): map_var pbc)
 End
 
 Definition edge_map_def:
   edge_map (a:num,b:num) (u:num) et =
-  (GreaterEqual,
-    (1,Neg (a,u)) :: MAP (λv. (1,Pos (b,v))) (neighbours et u),
-    1): map_var pbc
+  (
+  concat [strlit"adj"; toString a; strlit"_"; toString u; strlit"_"; toString b]
+  ,(GreaterEqual,
+    (1,Neg (a,u)) ::
+      MAP (λv. (1,Pos (b,v))) (neighbours et u),
+    1): map_var pbc)
 End
 
 Definition all_has_mapping_def:
   all_has_mapping vp vt =
-  GENLIST (λa. has_mapping a vt) vp
+  GENLIST (λa. has_mapping_al1 a vt) vp ++
+  GENLIST (λa. has_mapping_am1 a vt) vp
 End
 
 Definition all_one_one_def:
@@ -55,7 +67,9 @@ End
 
 Definition encode_def:
   encode (vp,ep) (vt,et) =
-  all_has_mapping vp vt ++ all_one_one vp vt ++ all_edge_map (vp,ep) (vt,et)
+  all_has_mapping vp vt ++
+  all_one_one vp vt ++
+  all_edge_map (vp,ep) (vt,et)
 End
 
 Theorem iSUM_zero:
@@ -246,7 +260,8 @@ Theorem encode_correct:
   good_graph (vp,ep) ∧
   good_graph (vt,et) ∧
   encode (vp,ep) (vt,et) = constraints ⇒
-  (has_subgraph_iso (vp,ep) (vt,et) ⇔ satisfiable (set constraints))
+  (has_subgraph_iso (vp,ep) (vt,et) ⇔
+    satisfiable (set (MAP SND constraints)))
 Proof
   rw[EQ_IMP_THM]
   >- (
@@ -256,17 +271,20 @@ Proof
     rw[encode_def]
     >- (
       rename1`all_has_mapping`>>
-      simp[all_has_mapping_def,satisfies_def,MEM_GENLIST,has_mapping_def]>>
-      rw[]>>
-      simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
-      DEP_REWRITE_TAC[iSUM_eq_1,eval_lin_term_def]>>
-      CONJ_TAC>-
-        (simp[MEM_GENLIST]>>metis_tac[])>>
-      qexists_tac`f a`>>
-      CONJ_ASM1_TAC>>fs[EL_GENLIST,INJ_DEF])
+      simp[all_has_mapping_def,satisfies_def,MEM_GENLIST,MEM_MAP,PULL_EXISTS]>>
+      `∀a. a < vp ⇒
+        iSUM (GENLIST (λv. b2i (f a = v)) vt) = 1` by (
+        rw[]>>
+        DEP_REWRITE_TAC[iSUM_eq_1,eval_lin_term_def]>>
+        CONJ_TAC>-
+          (simp[MEM_GENLIST]>>metis_tac[])>>
+        qexists_tac`f a`>>
+        CONJ_ASM1_TAC>>fs[EL_GENLIST,INJ_DEF])>>
+      rw[]>>first_x_assum drule>>
+      simp[satisfies_pbc_def,has_mapping_al1_def,eval_lin_term_def,MAP_GENLIST,o_DEF,has_mapping_am1_def])
     >- (
       rename1`all_one_one`>>
-      simp[all_one_one_def,satisfies_def,MEM_GENLIST,one_one_def]>>
+      simp[all_one_one_def,satisfies_def,MEM_GENLIST,one_one_def,MEM_MAP,PULL_EXISTS]>>
       rw[]>>
       simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
       fs[INJ_DEF]>>
@@ -286,7 +304,7 @@ Proof
       simp[])
     >- (
       rename1`all_edge_map`>>
-      simp[all_edge_map_def,satisfies_def,MEM_GENLIST,MEM_FLAT,edge_map_def]>>
+      simp[all_edge_map_def,satisfies_def,MEM_GENLIST,MEM_FLAT,edge_map_def,MEM_MAP,PULL_EXISTS]>>
       rw[]>>
       gvs[MEM_FLAT,MEM_GENLIST,MEM_MAP]>>
       fs[MEM_neighbours]>>
@@ -314,10 +332,15 @@ Proof
   `∀n. n < vp ⇒
     ∃m. m < vt ∧ w (n,m) ∧
     ∀m'. m' < vt ∧ w (n,m') ⇔ m = m'` by (
-    fs[all_has_mapping_def,MEM_GENLIST,has_mapping_def,PULL_EXISTS]>>
+    fs[all_has_mapping_def,MEM_GENLIST,has_mapping_al1_def,
+      has_mapping_am1_def,PULL_EXISTS,MEM_MAP,PULL_EXISTS,SF DNF_ss]>>
     rw[]>>
     first_x_assum drule>>
+    first_x_assum drule>>
     simp[satisfies_pbc_def,MAP_GENLIST,o_DEF,eval_lin_term_def]>>
+    rw[]>>
+    `iSUM (GENLIST (λv. b2i (w (n,v))) vt) = 1` by intLib.ARITH_TAC>>
+    pop_assum mp_tac>>
     DEP_REWRITE_TAC[iSUM_eq_1]>>
     CONJ_TAC>- (
       simp[MEM_GENLIST]>>metis_tac[])>>
@@ -327,6 +350,7 @@ Proof
     Cases_on`i=m'`>>gs[]>>
     first_x_assum drule>>
     fs[])>>
+  fs[MEM_MAP,PULL_EXISTS]>>
   rw[]
   >- (
     rw[INJ_DEF]
@@ -420,63 +444,34 @@ QED
 
 Definition full_encode_def:
   full_encode gp gt =
-  MAP (map_pbc enc_string) (FLAT (MAP pbc_ge (encode gp gt)))
+  MAP (SOME ## map_pbc enc_string) (encode gp gt)
 End
 
-(* TODO: move *)
-Theorem satisfies_set_FLAT:
-  pbc$satisfies w (set (FLAT ls)) ⇔
-  ∀x. MEM x ls ⇒ pbc$satisfies w (set x)
-Proof
-  rw[EQ_IMP_THM]>>fs[pbcTheory.satisfies_def,MEM_FLAT]>>
-  metis_tac[]
-QED
-
-Theorem satisfies_FLAT_MAP_pbc_ge:
-  satisfies w (set (FLAT (MAP pbc_ge pbf))) ⇔
-  satisfies w (set pbf)
-Proof
-  simp[satisfies_set_FLAT]>>
-  rw[EQ_IMP_THM]
-  >- (
-    rw[satisfies_def]>>fs[MEM_MAP,PULL_EXISTS]>>
-    first_x_assum drule>>
-    metis_tac[pbc_ge_thm])>>
-  fs[MEM_MAP]>>
-  metis_tac[pbc_ge_thm,satisfies_def]
-QED
-
-Theorem satisfiable_FLAT_MAP_pbc_ge:
-  satisfiable (set (FLAT (MAP pbc_ge pbf))) ⇔
-  satisfiable (set pbf)
-Proof
-  simp[satisfiable_def]>>
-  metis_tac[satisfies_FLAT_MAP_pbc_ge]
-QED
-
 Theorem full_encode_correct:
   good_graph gp ∧
   good_graph gt ⇒
-  (has_subgraph_iso gp gt ⇔ satisfiable (set (full_encode gp gt)))
+  (has_subgraph_iso gp gt ⇔
+    satisfiable (set (MAP SND (full_encode gp gt))))
 Proof
   rw[full_encode_def]>>
-  simp[LIST_TO_SET_MAP]>>
+  simp[LIST_TO_SET_MAP,IMAGE_IMAGE]>>
+  simp[Once (GSYM IMAGE_IMAGE)]>>
   DEP_REWRITE_TAC[satisfiable_INJ_iff]>>
   rw[]
   >- (
     assume_tac enc_string_INJ>>
     drule INJ_SUBSET>>
+    simp[IMAGE_IMAGE]>>
     disch_then match_mp_tac>>
     simp[])>>
-  simp[satisfiable_FLAT_MAP_pbc_ge] >>
-  metis_tac[encode_correct,PAIR,pbc_ge_thm]
+  metis_tac[encode_correct,PAIR,LIST_TO_SET_MAP]
 QED
 
 (* The theorem relating to sem_concl *)
 Theorem full_encode_sem_concl:
   good_graph gp ∧
   good_graph gt ∧
-  sem_concl (set (full_encode gp gt)) NONE concl
+  sem_concl (set (MAP SND (full_encode gp gt))) NONE concl
   ⇒
   case concl of
     DSat => has_subgraph_iso gp gt
@@ -491,7 +486,7 @@ QED
 Theorem full_encode_eq =
   full_encode_def
   |> SIMP_RULE (srw_ss()) [FORALL_PROD,encode_def]
-  |> SIMP_RULE (srw_ss()) [all_has_mapping_def,all_one_one_def,all_edge_map_def,has_mapping_def,one_one_def,edge_map_def]
+  |> SIMP_RULE (srw_ss()) [all_has_mapping_def,all_one_one_def,all_edge_map_def,has_mapping_al1_def,has_mapping_am1_def,one_one_def,edge_map_def]
   |> SIMP_RULE (srw_ss()) [MAP_FLAT,MAP_GENLIST,MAP_APPEND,o_DEF,MAP_MAP_o,pbc_ge_def,map_pbc_def,FLAT_FLAT,FLAT_MAP_SING,map_lit_def]
   |> SIMP_RULE (srw_ss()) [FLAT_GENLIST_FOLDN,FOLDN_APPEND,FOLDN_APPEND_op]
   |> PURE_ONCE_REWRITE_RULE [APPEND_OP_DEF]