diff --git a/easycrypt.project b/easycrypt.project
index 0c9ad34..25bac23 100644
--- a/easycrypt.project
+++ b/easycrypt.project
@@ -1,5 +1,5 @@
 [general]
 timeout = 10
-provers = Alt-Ergo@2.4
+provers = Alt-Ergo@2.5
 provers = CVC5@1.0
-provers = Z3@4.12
\ No newline at end of file
+provers = Z3@4.12
diff --git a/proofs/acai/FL_XMSS_TW.ec b/proofs/acai/FL_XMSS_TW.ec
index 0ed1f37..6807fea 100644
--- a/proofs/acai/FL_XMSS_TW.ec
+++ b/proofs/acai/FL_XMSS_TW.ec
@@ -220,8 +220,9 @@ proof. smt(list2tree_ok). qed.
 lemma list2tree1 (x : 'a) :
   list2tree [x] = Leaf x.
 proof.
-move: (list2tree_lvb [x] 0 0 _) => //.
-by rewrite expr0 /= int2bs0s /#.
+move: (list2tree_lvb [x] 0 0 _)=> //.
+rewrite expr0 /= int2bs0s rev_nil.
+by case: (list2tree [x]).
 qed.
 
 lemma list2tree_uniq2 ['a] (e : int) (s : 'a list) (t1 t2 : 'a bintree) :
diff --git a/proofs/fsai/FL_XMSS_TW.ec b/proofs/fsai/FL_XMSS_TW.ec
index 874d2ae..3a0e88c 100644
--- a/proofs/fsai/FL_XMSS_TW.ec
+++ b/proofs/fsai/FL_XMSS_TW.ec
@@ -369,7 +369,8 @@ lemma list2tree1 (x : 'a) :
   list2tree [x] = Leaf x.
 proof.
 move: (list2tree_lvb [x] 0 0 _) => //.
-by rewrite expr0 /= int2bs0s /#.
+rewrite expr0 /= int2bs0s rev_nil.
+by case: (list2tree [x]).
 qed.
 
 lemma list2tree_uniq2 ['a] (e : int) (s : 'a list) (t1 t2 : 'a bintree) :