diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index c1bc3500eac4a4764b0142fe08c04d7aa4eebba4..b1abfb6af8f8d565f167aa4674e9632c2423a3eb 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -323,7 +323,7 @@ struct
     let low = M.is_init_range sigma obj loc e_one in
     let lemma = p_equiv high low in
     {
-      l_assumed = true ;
+      l_kind = `Axiom ;
       l_name = name ^ "_low" ; l_types = 0 ;
       l_forall = F.p_vars lemma ;
       l_triggers = [] ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index e910305304a72d73a711b92d153b3de29defb6c2..3536f05e422c7ae63c3a0cb4e889d1e8fedb8087 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -546,7 +546,7 @@ module BASE = WpContext.Generator(Varinfo)
             let m_init = p_call p_cinits [m] in
             let init_prop = p_forall [a] (p_imply m_init init_access) in
             Definitions.define_lemma {
-              l_assumed = true ;
+              l_kind = `Axiom ;
               l_name = prefix ^ "_init" ; l_types = 0 ;
               l_triggers = [] ; l_forall = [] ;
               l_lemma = init_prop ;