Non-terminating typechecking when a lemma ends with `assert`

[funemy]

I'm running into this non-terminating issue when bumping my F* version to the most recent one.

I believe the issue was due to changes introduced in #4515.

Here is a minimal example crafted from my code.

module FinalAssertHang

open FStar.UInt

type pair = p: (uint_t 64 & uint_t 64) { let (a, b) = p in a < 16 /\ b < 16 }

let enc (p: pair) : uint_t 64 =
  let (a, b) = p in
  logor a (shift_left b 4)

let dec (op: uint_t 64) : uint_t 64 & uint_t 64 =
  (logand op (to_uint_t 64 0xF), logand (shift_right op 4) (to_uint_t 64 0xF))

// Verifies: the body ends in `()`
let roundtrip_ok (p: pair) : Lemma (ensures dec (enc p) == p) =
  let (a, b) = p in
  admit ();
  assert (logand (shift_right (enc p) 4) (to_uint_t 64 0xF) == b);
  ()

// Non-terminating: the body ends in `assert`
let roundtrip_hangs (p: pair) : Lemma (ensures dec (enc p) == p) =
  let (a, b) = p in
  admit ();
  assert (logand (shift_right (enc p) 4) (to_uint_t 64 0xF) == b)

The actual logic of the code probably doesn't matter too much.
From what I can understand in #4515, assert p now has the type squash p instead of unit.
The type checker will unify the asserted proposition with the post condition of the function, and it seemed that the normalizer fails to terminate when unfolding the types?

While the fix (i.e., by adding a () after the last assertion) was simple, the issue was quite annoying in practice.