- added axiom of undefined
- enhanced presentation: axioms, results
- minor style fixes
- added lemma of equiv diffs
- reproved both theorems