ABSTRACT
With this interpretation a complete axiomatic basis for LPC with identity may be provided by adding the axiom
II x = x
and the axiom schema
12 x = y D (a D 0)
where a and /? differ only in that a has free x in 0 or more places where jS has free y.