Expose lemma and path in Proof

[nazar-pc]

Can you expose Proof's path and lemma properties?

This is really a requirement for the library to be usable since otherwise created proof can't be stored anywhere.