_______ 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