proposition: Lemma normal_ofs_uniqueness1 f g (p:fterm) u: normal_ofs1 f u -> normal_ofs1 g u -> ordinalp u -> (forall x, u <=o x -> f (osucc x) = p (f x)) -> (forall x, u <=o x -> g (osucc x) = p (g x)) -> (f u = g u) -> (forall x, u <=o x -> f x = g x).
proof: Proof. move => [pa pb] [pc pd] ou pe pf pg x cp. have ox:= proj32 cp. move: x ox cp. apply: least_ordinal2 => y p1 p3 yp. case:(ole_eqVlt yp); [by move <- | move => uny]. case: (ordinal_limA p1). - by move => y0; case: (@olt0 u); rewrite - y0. - move => [t ot st]; rewrite st; rewrite st in p1. have h : u <=o t by apply /oltSleP; rewrite - st. move: (oltS (proj32 h)); rewrite - {1} st => ty. by rewrite (pe _ h) (pf _ h) (p3 _ ty h). - move => ly. set E := ordinal_interval u y. have uu:=(oleR (proj31 yp)). have pe1: (forall x, inc x E -> u <=o x) by move => t/(ointvP p1) []. have pe2: nonempty E by exists u; apply /(ointvP p1). have pe3: \osup E = y by rewrite (ointv_sup1 uny ly). move: (pb _ pe1 pe2) (pd _ pe1 pe2); rewrite pe3 => <- <-. by apply:ord_sup_2funI => s /(ointvP p1) [s1 s2]; apply: p3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)