Hello,

There is a nice theorem prover for propositional logic with LK implemented in Prolog here:

the output for the example

```
prove0(((a & b) => a), Proof).
```

is the following one:

```
Proof = rimpl([]>[(a&b=>a)],land([(a&b)]>[a],ax([a,b]>[a],a))).
```

I wonder how to capitalize the atoms to get from this second output instead of the first one:

```
Proof = rimpl([]>[(A&B=>A)],land([(A&B)]>[B],ax([B,B]>[A],A))).
```

Because I guess that the image of the sequent proof wich is provided by the LateX macro bussproofs.sty implemented in MathJax would give variables in uppercase via the Tau Prolog script. Ido not doubt that such a program could also be written in SWI-Prolog, but I prefer to focus on the use of upcase_atom/2 for this leanseq.pl program or on any lines of Prolog code to get propositional variables in uppercase.

Thanks for your help or your suggestions !

Jo.