proposition: Lemma cantor_unique a n b a' n' b': T1nf (cons a n b) -> T1nf (cons a' n' b') -> (T1omega^a) * (\F n.+1) + b = (T1omega^a') * (\F n'.+1) + b' -> (a=a' /\ n = n' /\ b = b').
proof: Proof. by move => /cantor_exists <- /cantor_exists <-; case. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)