proposition: Lemma ord_induction_yp w0 g x (f:= (ord_induction_defined w0 g)): (forall y, \0o <o y -> f x y = ord_induction_sup g x y (f x)).
proof: Proof. move => y [[_ oy _] ynz]. rewrite /f /ord_induction_defined. rewrite (transdef_ord_pr (ord_induction_p w0 g x) oy). rewrite /transdef_ord_prop {1} /ord_induction_p; aw; Ytac0. apply: ord_sup_2funI => t ty /=; rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)