proposition: Lemma all_der_unique f1 f2 b1 b2 (g1:= all_der f1 b1) (g2:= all_der f2 b2): normal_ofs f1 -> all_der_bound f1 b1 -> all_der_bound f2 b2 -> (f1 =1o f2) -> (forall x i, ordinalp x -> ordinalp i -> g1 x i = g2 x i).
proof: Proof. move => nf1 h1 h2 sv. have nf2 := (normal_ofs_from_exten sv nf1). move => x i ox oi; move: i oi x ox; apply:least_ordinal2 => y oy etc. case: (ozero_dichot oy) => yp. rewrite yp => x ox. by rewrite /g1 /g2 (all_der_p2 nf1 h1 ox)(all_der_p2 nf2 h2 ox) sv. move: (all_der_p6 nf1 h1 oy); rewrite -/g1; move=> [pa _]. move: (all_der_p6 nf2 h2 oy); rewrite -/g2; move=> [pb _]. apply:(sincr_ofs_exten pa pb) => x ox. move:(ofs_sincr pa ox) => sa. apply:(all_der_p8 nf2 h2 sa yp). move => j jy; rewrite -/g2 - (etc j jy _ sa). exact :(all_der_p7 nf1 h1 ox jy). move:(ofs_sincr pb ox) => sa. apply:(all_der_p8 nf1 h1 sa yp). move => j jy;rewrite -/g1 (etc j jy _ sa). exact :(all_der_p7 nf2 h2 ox jy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)