Here is a minimal theorem prover in Prolog:

:- op(1110, xfy, =>).   % conditional
% -----------------------------------------------------------------
provable(F,P):-
        prove([]>[F],P).
% -----------------------------------------------------------------
%% 1. Initial rule: if G and D are strings [i.e. lists] of atomic formulae,
%% then G > D  is a theorem if some atomic formula occurs on both sides of the arrow:                 
prove(G>D, ax(G>D, A)):-
        member(A,G), member(B,D), A==B,!.

%% 2. Conditional on the  right 
prove(G>D, rcond(G>D,P)):-
        select((A=>B),D,D1),!,
        prove([A|G]>[B|D1],P).

to prove identity :

?- provable((p => p), Proof).
Proof = rcond([]>[(p=>p)], ax([p]>[p], p)).

I do not succeed to write some lines of Prolog code to get with the same input i.e.

?- provable((p => p), Proof).

an output with atomic variables in capital letters i.e.

Proof = rcond([]>[(P=>P)], ax([P]>[P], P)).

I am aware that

?- provable(('P' => 'P'), Proof).

is a workaround that solves the problem, but I'm searching a better solution, less tedious or more user-friendly.

Any help is welcome. Thanks !