proposition: Lemma normal_ofs_uniqueness f g (p:fterm): normal_ofs f -> normal_ofs g -> (forall x, ordinalp x -> f (osucc x) = p (f x)) -> (forall x, ordinalp x -> g (osucc x) = p (g x)) -> (f \0o = g \0o) -> f =1o g.
proof: Proof. move => pa pb pc pd pe y oy. have pa':= (normal_ofs_equiv2 OS0 pa). have pb':= (normal_ofs_equiv2 OS0 pb). have pc':(forall x, \0o <=o x -> f (osucc x) = p (f x)). by move => x xp; apply: pc (proj32 xp). have pd':(forall x, \0o <=o x -> g (osucc x) = p (g x)). move => x xp; apply: pd (proj32 xp). apply:(normal_ofs_uniqueness1 pa' pb' OS0 pc' pd' pe); apply:(ole0x oy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)