proposition: Lemma ord_induction_y0 w0 g x: ord_induction_defined w0 g x \0o = w0 x.
proof: Proof. rewrite /ord_induction_defined (transdef_ord_pr (ord_induction_p w0 g x) OS0). by rewrite /ord_induction_p; aw; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)