proposition: Lemma T1T3_surj x: T3nf x -> x < epsilon0 -> exists y, x = T1_T3 y.
proof: Proof. set n := (size x).+1. move: (leqnn n); rewrite {1}/n; move: n => n. elim: n x => [ // | n Hr x]. case x; first by exists CantorOrdinal.zero => //. move => a' b' c' n' d'; rewrite ltnS => lu nc. move /and5P: (size_prop1 a' b' c' n' d') => [la lb lc ld _]. rewrite lt_epsilon0; move => /and3P [sa sb sc]. move: nc; rewrite nf_consE nf_psi => /and3P [/and3P [_ _ nc] nd ne]. rewrite (eqP sa) (eqP sb). have [y yp]:= (Hr c' (leq_trans lc lu) nc sc). have ww: [a', b', c'] < [zero, one, zero] by rewrite lt_epsilon0 /= sa sb sc. have [y' yp'] := (Hr d' (leq_trans ld lu) nd (T3lt_trans ne ww)). by exists (CantorOrdinal.cons y n' y') => /=; rewrite -yp - yp'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)