"infinity (non-negative integers with infinity)"
'Infinity = yinf.
-(* Inversion lemmas *********************************************************)
+(* Inversions ***************************************************************)
(* Note: destruct *)
(*** yinj_inj *)
#x #y #H destruct //
qed-.
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** eq_ynat_dec *)
lemma eq_ynat_dec (y1,y2:ynat): Decidable (y1 = y2).