app([],L,L).
app([E|R],L,[E|RL]) :- app(R,L,RL).

% Prolog-Interpreter:
prove(true) :- !.
prove( (A,B) ) :- !, prove(A), prove(B).
prove( A ) :- clause(A,G), prove(G).

% Prolog-Interpreter mit Beweislaengenberechnung:
lprove(true,0) :- !.
lprove( (A,B), L) :- !, lprove(A,LA), lprove(B,LB), L is LA+LB.
lprove( A, L) :- clause(A,G), lprove(G,LG), L is LG+1.
