proposition: Lemma ord_index_pr n: ordinalp n -> ord_index (\aleph n) = n.
proof: Proof. move => on; move: (CIS_aleph on) => /ord_index_pr1 [h1 h2]. exact: (aleph_inj h1 on h2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)