Pf2

Pf2 is a LaTexX package designed by Leslie Lamport that allows to make very beautiful proof.

http://us2.metamath.org:88/downloads/inpreima2.pdf

I just want to make two remarks.

First I don't undertand why the "let" is not indented. A "let" belongs to a proof like the other parts of this

proof (assumption and steps). It is simply an assumption that occurs when you remove a forall (in a bottom-up way).

Moreover, the variable has a range and cannot be used outside of it and

if you don't indent it you can't see where the range begins and where it stops.

Second. We should be able to add a comment by a QED step. It's a step in its own right. Currently

one can only add a comment below contrary to what happens with the other steps. But very often

the comment is small and putting it on the same line as the QED would be preferable.