`hax_lib::lemma` introduces a `True` literal that shouldn't be there

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Still relevant

#[hax_lib::lemma]
fn hello() -> Proof<true> {}

Open this code snippet in the playground

Extracts to:

module Playground
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

let hello (_: Prims.unit)
    : Lemma Prims.l_True (ensures true) =
  ()