Box

If A is a proposition and a : A, then \box a : A is an element that does not evaluate to anything, but which is judgmentally equal to any other boxed element. This includes all expressions of the form \box b and also all lemma calls.

If the type of a parameter of a definition is a proposition, this parameter can be marked with \property keyword. Then the corresponding argument will be automatically surrounded in \box for every call of this definition.