proposition: Lemma strong_critical_closed_proper: iclosed_proper (fun z => ordinalp z /\ strong_critical z).
proof: Proof. move: Sphi_p5;set f := (Sphi^~ \0o) => nf. move: (iclosed_fixpoints nf) => [[pa pb] pc]. have aux z: (ordinalp z /\ strong_critical z) <-> (ordinalp z /\ f z = z). split. by move => [oz] /(strong_criticalP oz). by move => [oz] /(strong_criticalP oz). split => //; first split. + by move => x []. + by move => g pF nef; apply /aux; apply: pb => // x/pF => /aux w. + by move => [E ev]; case:pc; exists E => x; split; [move/ev/aux| move/aux/ev]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)