proposition: Lemma CNF_simple_unique a n b a' n' b' x: CNF_simple_ax a n b x -> CNF_simple_ax a' n' b' x -> [/\ a = a', b = b' & n = n'].
proof: Proof. move => ha1 hb1. move: (ha1)(hb1) => / CNF_simple_p1 ha / CNF_simple_p1 hb. have osx : ordinalp x by move:ha => [oa ob oc [-> _ _ _]]; fprops. move: (ord_ext_div_unique ole_2omega osx ha hb) => [hd he hf]. move: ha1 hb1 => [ _ _ /CS_nat cn _ _] [ _ _ /CS_nat cn' _ _]. by split => //; apply:csucc_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)