proposition: Lemma Spsi_p4 a a' b b': ordinalp a -> ordinalp a' -> ordinalp b -> ordinalp b' -> (Spsi a b = Spsi a' b') -> (a = a' /\ b = b').
proof: Proof. move=> oa oa' ob ob' eq. move: (Spsi_p1' oa ob); set c := Yo _ _ _. move: (Spsi_p1' oa' ob'); set c' := Yo _ _ _. move => sa sb. move /(Sphi_p6 (proj31_1 sb) (proj31_1 sa) oa oa') : (eq). move => [qa qb qc]. have eq0:Sphi a c = Sphi a' c' by []. case: (oleT_ell oa oa') => h. + case: (oleT_ell ob ob') => h'; first by split. move:(Spsi_p3 oa h') => [_]; rewrite eq h; case; reflexivity. move:(Spsi_p3 oa h') => [_]; rewrite eq h;case; reflexivity. + by move: (qa h); move: sb => [_ hu]; rewrite - eq0 => hv; case: hu. + by move: (qc h); move: sa => [_ hu]; rewrite eq0 => hv; case: hu. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)