LSP: Create proof step markers for USE statements involving facts.

[kape1395]

Fixes #192

[kape1395]

Some changes are caused by the ocamlformat, which started formatting the comments after its version was updated. I will create another PR to re-format other files under ./lsp.

[ahelwer]

Is there a reason this was not done previously? Are USE steps exposed in some strange way through the parse tree? Was it just not implemented yet, as shown by this line?

  | Proof.T.Use (_, _) -> (None, acc)

[kape1395]

I skipped them when implementing the LSP mainly because these steps were not marked "green" in the toolbox. So, I assumed they produce no proof obligations. Now I understand they do.