I am not questioning or criticizing, just curious - why was it decided to implement lemmas as terms? I guess it is for code reuse purposes, but just wanted to ask.

Cheers,

Denny