# Adding equality to the 'calcprop' theory. param (CALCPROPEQ pax/calcpropeq (CALCPROP) "") var (value a b c) stmt (inf-=comm () ((= a b)) (= b a))