Make e<>f and e#f irrelevant

Though True/False are being used, not using proof irrelevance creates
trouble in equality of chains
Introduce axioms for Incidence Plane
Lemma 2.4 : Initial commit

* Define functions that take ppchains to chains and back
* prove that they compose to respective identies