`tt` is sometimes not translated

[gebner]

trafficstars

Mathlib (data/nat/basic):

@[simp] lemma bodd_bit1 (n) : bodd (bit1 n) = tt := bodd_bit tt n

Synport:

@[simp]
theorem bodd_bit1 (n) : bodd (bit1 n) = tt :=
  bodd_bit true n

This instance shows both tt being translated to true, as well as tt not being translated.

[gebner]

This happens because only the second tt has a resolved constant in the AST. Not sure why there is a difference between theorem statement and proof here.