proposition: Lemma inv_psi_omega_p x (z:= oopow x) (y:= inv_psi_omega x) : ordinalp x -> [/\ pairp y, (P y) <=o z, (Q y) <o z & Spsip y = z].
proof: Proof. move => ox. pose p z:= (Spsip z = oopow x). set E := (coarse (osucc (oopow x))). have oo:= OS_oopow ox. have osx:= (OS_succ oo). have pb:singl_val2 (inc^~ E) p. move => y1 y2 /setX_P [ra rb rc] e1 /setX_P [ra' rb' rc']. rewrite /p - e1 => e2. move: (Os_ordinal osx rb) (Os_ordinal osx rc) => o1 o3. move: (Os_ordinal osx rb') (Os_ordinal osx rc') => o2 o4. move:(Spsi_p4 o2 o1 o4 o3 e2) => [rd re]. by apply: pair_exten. move: (Spsi_p7 (indecomp_prop4 ox)) => [a [b [p1 p2 p3]]]. have p4: (inc (J a b) E). move:(p2) =>[p2' _]; apply/setX_P; aw; split; fprops; by apply/oleP. have p5: p (J a b) by rewrite /p/Spsip; aw. move: (select_uniq pb p4 p5); rewrite /y /inv_psi_omega; move => <-; aw. rewrite p5; split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)