(* Advanced eliminators *****************************************************)
lemma nta_ind_rest_cnv (h) (Q:relation4 …):
- (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+ (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
(∀G,K,V,W,U.
⦃G,K⦄ ⊢ V :[h] W → ⬆*[1] W ≘ U →
Q G K V W → Q G (K.ⓓV) (#0) U
/4 width=5 by nta_bind_cnv/
| #V #T #HG #HL #HT #X #H destruct
elim (nta_inv_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX
- /4 width=9 by nta_appl/
+ /4 width=9 by nta_appl, ylt_inj/
| #U #T #HG #HL #HT #X #H destruct
elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
/4 width=4 by nta_cast/
qed-.
lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
- (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+ (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
(∀G,K,V,W,U.
⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
Q G K V W → Q G (K.ⓓV) (#0) U
qed-.
lemma nta_ind_ext_cnv (h) (Q:relation4 …):
- (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+ (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
(∀G,K,V,W,U.
⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
Q G K V W → Q G (K.ⓓV) (#0) U
lapply (nta_fwd_cnv_dx … HTU) #H
elim (cnv_inv_bind … H) -H #_ #HU
elim (cnv_nta_sn … HU) -HU #X #HUX
-/4 width=2 by nta_beta, nta_fwd_cnv_sn/
+/4 width=2 by nta_appl_abst, nta_fwd_cnv_sn/
qed-.