proposition: Lemma ord_induction_unique (w0: fterm) (g:fterm2) u (f f':fterm2) (P := fun f => forall x, u <=o x -> ( f x \0o = w0 x /\ (forall y, \0o <o y -> f x y = ord_induction_sup g x y (f x)))): P f -> P f' -> forall x, u <=o x -> f x =1o f' x.
proof: Proof. move => pa pb x ux; apply:least_ordinal2 => y oy lpy. move: (pa _ ux) (pb _ ux) => [h1 h2] [h3 h4]. case: (ozero_dichot oy) => ey0; first by rewrite ey0 h1. rewrite (h2 _ ey0)(h4 _ ey0). by apply: ord_sup_2funI => z /(oltP oy) /lpy ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)