diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml
index 07a364ed3..b93ceca0d 100644
--- a/backend/cn/lib/cn_internal_to_ail.ml
+++ b/backend/cn/lib/cn_internal_to_ail.ml
@@ -13,6 +13,7 @@ open Mucore
 module A = CF.AilSyntax
 module C = CF.Ctype
 module BT = BaseTypes
+module IT = IndexTerms
 module T = Terms
 module LRT = LogicalReturnTypes
 module LAT = LogicalArgumentTypes
@@ -1488,6 +1489,17 @@ let cn_to_ail_expr_internal
   fun dts globals cn_expr d -> cn_to_ail_expr_aux_internal None None dts globals cn_expr d
 
 
+let cn_to_ail_expr
+  (dts : _ CF.Cn.cn_datatype list)
+  (globals : (C.union_tag * C.ctype) list)
+  (it : IT.t)
+  : A.bindings
+    * CF.GenTypes.genTypeCategory A.statement_ list
+    * CF.GenTypes.genTypeCategory A.expression
+  =
+  cn_to_ail_expr_internal dts globals it PassBack
+
+
 let cn_to_ail_expr_internal_with_pred_name
   : type a.
     Sym.sym option ->
diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli
index 1705dbcb5..389261f03 100644
--- a/backend/cn/lib/cn_internal_to_ail.mli
+++ b/backend/cn/lib/cn_internal_to_ail.mli
@@ -3,6 +3,7 @@ module A = CF.AilSyntax
 module C = CF.Ctype
 module BT = BaseTypes
 module AT = ArgumentTypes
+module IT = IndexTerms
 
 val ownership_ctypes : C.ctype list ref
 
@@ -18,6 +19,12 @@ val records : Sym.t RecordMap.t ref
 
 val bt_to_cn_base_type : BT.t -> Sym.t CF.Cn.cn_base_type
 
+val bt_to_ail_ctype : ?pred_sym:Sym.t option -> BT.t -> C.ctype
+
+val wrap_with_convert_from_cn_bool
+  :  CF.GenTypes.genTypeCategory A.expression ->
+  CF.GenTypes.genTypeCategory A.expression
+
 val generate_sym_with_suffix
   :  ?suffix:string ->
   ?uppercase:bool ->
@@ -85,6 +92,14 @@ val generate_record_map_get
   :  Sym.t * 'a ->
   (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list
 
+val cn_to_ail_expr
+  :  A.sigma_cn_datatype list ->
+  (C.union_tag * C.ctype) list ->
+  IT.t ->
+  A.bindings
+  * CF.GenTypes.genTypeCategory A.statement_ list
+  * CF.GenTypes.genTypeCategory A.expression
+
 val cn_to_ail_struct : A.sigma_tag_definition -> A.sigma_tag_definition list
 
 val cn_to_ail_datatype