lemma ysucc_inf: ∞ = ↑(∞).
// qed.
-(* Inversion lemmas *********************************************************)
+(* Inversions ***************************************************************)
(*** ysucc_inv_inj_sn *)
lemma eq_inv_inj_ysucc (n1) (x2):
#x1 @(ynat_split_nat_inf … x1) -x1
[ #n1 #x2 <ysucc_inj #H
elim (eq_inv_inj_ysucc … H) -H #n2 #H1 #H2 destruct
- /3 width=1 by eq_inv_nsucc_bi, eq_f/
+ <(eq_inv_nsucc_bi … H2) -H2 //
| #x2 #H <(eq_inv_inf_ysucc … H) -H //
]
qed-.
lemma eq_inv_ysucc_zero (x): ↑x = 𝟎 → ⊥.
/2 width=2 by eq_inv_zero_ysucc/ qed-.
-(* Eliminators **************************************************************)
+(* Eliminations *************************************************************)
(*** ynat_ind *)
lemma ynat_ind_succ (Q:predicate …):