Fix a notation issue in previous commit

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 85d2ac89a..00f446811 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1993,7 +1993,7 @@ Proof. rewrite <- combine_map_map with (g:=f) (f:=fun x => x), map_id; reflexivi
 Lemma combine_same A xs
   : @combine A A xs xs = map (fun x => (x, x)) xs.
 Proof. induction xs; cbn; congruence. Qed.
-Lemma if_singleton A (b:bool) (x y : A) : (if b then [x] else [y]) = [if b then x else y].
+Lemma if_singleton A (b:bool) (x y : A) : (if b then x::nil else y::nil) = (if b then x else y)::nil.
 Proof. now case b. Qed.
 Lemma flat_map_if_In A B (b : A -> bool) (f g : A -> list B) xs (b' : bool)
   : (forall v, In v xs -> b v = b') -> flat_map (fun x => if b x then f x else g x) xs = if b' then flat_map f xs else flat_map g xs.