proposition: Lemma transdef_ord_pr (p:fterm) x: ordinalp x -> transdef_ord_prop p (transdef_ord p) x.
proof: Proof. pose F y := (transfiniteg_defined (ordinal_o y) p). have ha: forall y, ordinalp y -> worder (ordinal_o y). by move => y oy; apply:ordinal_o_wor. have hb: forall y, ordinalp y -> transfiniteg_def (ordinal_o y) p (F y). move => y oy; apply: (transfinite_pr1 p (ha _ oy)). have hd: forall y z g, ordinalp y -> inc z y -> p (restr g (segment (ordinal_o y) z )) = p (Lg z (Vg g)). move => y z g oy zy. by rewrite (ordinal_segment oy zy) /restr. have he: forall y z, z <o y -> Vg (F y) z = p (Lg z (Vg (F y))). move => y z /oltP0 [oz oy lzy]; move: (hb _ oy) => [pa pb pc]. by rewrite - (hd _ _ _ oy lzy);apply: pc; rewrite ordinal_o_sr. have he': forall y z, ordinalp y -> inc z y -> Vg (F y) z = p (Lg z (Vg (F y))). move => y z oy lzy; move: (hb _ oy) => [pa pb pc]. by rewrite - (hd _ _ _ oy lzy);apply: pc; rewrite ordinal_o_sr. have hc: forall z, ordinalp z -> forall y1 y2, z <o y1 -> z <o y2 -> Vg (F y1) z = Vg (F y2) z. apply: least_ordinal2 => b ob bp y1 y2 lt1 lt2. rewrite (he _ _ lt1) (he _ _ lt2). f_equal; apply:Lg_exten => s /(oltP (proj31_1 lt1)) sb; apply: (bp _ sb). apply: (olt_ltT sb lt1). apply: (olt_ltT sb lt2). move => ox;set f := (transdef_ord p). hnf; have <-: Vg (F (osucc x)) x = f x by []. rewrite (he _ _ (oltS ox)); f_equal; apply: Lg_exten. move => t /(oltP ox) ltx; move:(proj31_1 ltx) => ot. apply: (hc _ ot) (olt_ltT ltx (oltS ox)) (oltS ot). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)