proposition: Lemma Gamma0_s_psi a b: a <o Gamma_0 -> b <o Gamma_0 -> Spsi a b <o Gamma_0.
proof: Proof. move => pa pb; rewrite /Spsi; Ytac h; apply:Gamma0_s => //. by move /limit_ordinal_P: Gamma0_limit => [_ ]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)