proposition: Lemma Sphi_p10a a b a' b' x: ordinalp a -> b <o x -> x = Sphi a b -> ordinalp a' -> b' <o x -> x = Sphi a' b' -> (a = a' /\ b = b').
proof: Proof. move => oa p2 p3 oa' q2 q3. rewrite p3 in q3. move/ (Sphi_p6 (proj31_1 p2) (proj31_1 q2) oa oa'): (q3). move => [sa sb sc]. case: (oleT_ell oa oa') => h; first by split => //; apply: sb. by move: (sa h) p2; rewrite - q3 - p3 => ->; move => []. by move: (sc h) q2; rewrite - p3 => ->; move => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)