Normalizer has weird behavior with one-element lists (again)

[TWal]

Following the resolution of #3353, I can now use my squash (norm ...) construct in my proofs, however, I need to prove it first! I am again noticing a weird behavior when the list has only one element, see below:

// true when all elements of a list satisfy a predicate
let rec for_allP (#a:Type) (pre:a -> prop) (l:list a): prop =
  match l with
  | [] -> True
  | h::t -> pre h /\ for_allP pre t

// a type, a predicate on that type, and some values
assume val ty: Type0
assume val pre: ty -> prop

assume val v1: ty
assume val v2: ty
assume val v3: ty

// some useful lemma
assume val all_pre_lemma:
  l:list ty ->
  Lemma (for_allP pre l)

let all_v = [ v1; v2; v3 ]

// We want to have the normalization of `all_pre_lemma`'s post-condition in the context
// This works well
#push-options "--fuel 0 --ifuel 0"
val all_v_pre: squash (norm [delta_only [`%all_v; `%for_allP]; iota; zeta] (for_allP pre all_v))
let all_v_pre =
  all_pre_lemma all_v;
  norm_spec [delta_only [`%all_v; `%for_allP]; iota; zeta] (for_allP pre all_v)
#pop-options

assume val v4: ty

// But when the list only has one element...
let all_v_one = [ v4; ]

// this fails without fuel
#push-options "--fuel 0 --ifuel 0"
val all_v_one_pre: squash (norm [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one))
let all_v_one_pre =
  all_pre_lemma all_v_one;
  norm_spec [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one)
#pop-options

The workaround is to use a fuel of 1, which is not too bad, but I am still posting this issue for posterity.

Another workaround is this:

#push-options "--fuel 0 --ifuel 0"
val all_v_one_pre: squash (norm [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one))
let all_v_one_pre =
  all_pre_lemma all_v_one;
  norm_spec [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one);
  let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in
  dumb_lemma (for_allP pre all_v_one) (norm [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one))
#pop-options