_______ Ref
s = t t = t
------------------------------- \rho mit C = \lambda x. t = x
t = s
geht datt?
datt geht dann, wenn links dat s = t vorher mit sym vertauscht wurde zu t = s weil die linken seiten verbastelt werden:
also
s = t
--------- sym _________ Ref
t = s t = t
----------------------------------
s = t
so hab ich das jedenfalls mal verstanden
aber annersrum passts... haha! *freu*
_______ Ref
s = t s = s
------------------------------- \rho mit C = \lambda x. x = s
t = s