/2 width=2 by ysucc_inv_O_sn/ qed-.
(* Eliminators **************************************************************)
lemma ynat_ind: ∀R:predicate ynat.
/2 width=2 by ysucc_inv_O_sn/ qed-.
(* Eliminators **************************************************************)
lemma ynat_ind: ∀R:predicate ynat.