is mentioned by

Thm* t:(u Term), x:u. (t = x) Prop

[reps_wf]