% Programmiere T[X/S]

% T = Var | Atom | (R * S) | lam(Var,T)

% subst(T,[X/S],-Ergebnis).

subst(T,[X/S],Ergebnis) :-
    var(T), !,
    (T == X -> Ergebnis = S ; Ergebnis = T).
subst(T,[X/S],T) :-
    atom(T).
subst(R * T, [X/S], Ergebnis) :-
    subst(R,[X/S],ER),
    subst(T,[X/S],ET),
    Ergebnis = (ER * ET).
% Voraussetzung: keine freie Var von S kommt in T gebunden vor. 
subst(lam(Y,T),[X/S],Ergebnis) :-
    (X == Y -> Ergebnis = lam(Y,T)
    ; subst(T,[X/S],ET),
        Ergebnis = lam(Y,ET)
    ).