proposition: Lemma Cantor_eta_pr2: Cantor_eta +t \1t <> Cantor_eta.
proof: Proof. move:BQ_int01_or_osr => [or1 sr1]. move: (set1_wor emptyset) => [[or2 _] sr2]. move: (orsum2_osr or1 or2) => [pc pd]. rewrite (OT_sum2_pr2 or1 or2); move /(Cantor_etaP pc). rewrite -/singleton_order. move => [[qa qb _ qd _] _]. move: pd; rewrite sr2 sr1; set E := canonical_du2 _ _ => pd. have xE: inc (J emptyset C1) E by apply:candu2_prb; fprops. rewrite pd in qd; move: (qd _ xE) => [y [/orsum2_gleP [_ yE lxy]] nexy]. move /candu2P: yE => [ya yb]. move: lxy; aw; case; move => []; fprops => sa sb;case: yb; move => [sc sd] //. by move/set1_P => /pr2_def h; case nexy; symmetry;apply: pair_exten; fprops; aw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)