(* Advanced properties ******************************************************)
lemma nta_ldef (h) (a) (G) (K):
- â\88\80V,W. â¦\83G,Kâ¦\84 ⊢ V :[h,a] W →
- ∀U. ⇧*[1] W ≘ U → ⦃G,K.ⓓV⦄ ⊢ #0 :[h,a] U.
+ â\88\80V,W. â\9d¨G,Kâ\9d© ⊢ V :[h,a] W →
+ ∀U. ⇧[1] W ≘ U → ❨G,K.ⓓV❩ ⊢ #0 :[h,a] U.
#h #a #G #K #V #W #H #U #HWU
elim (cnv_inv_cast … H) -H #X #HW #HV #HWX #HVX
lapply (cnv_lifts … HW (Ⓣ) … (K.ⓓV) … HWU) -HW
qed.
lemma nta_ldec_cnv (h) (a) (G) (K):
- â\88\80W. â¦\83G,Kâ¦\84 ⊢ W ![h,a] →
- ∀U. ⇧*[1] W ≘ U → ⦃G,K.ⓛW⦄ ⊢ #0 :[h,a] U.
+ â\88\80W. â\9d¨G,Kâ\9d© ⊢ W ![h,a] →
+ ∀U. ⇧[1] W ≘ U → ❨G,K.ⓛW❩ ⊢ #0 :[h,a] U.
#h #a #G #K #W #HW #U #HWU
lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU)
/3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/
qed.
lemma nta_lref (h) (a) (I) (G) (K):
- â\88\80T,i. â¦\83G,Kâ¦\84 ⊢ #i :[h,a] T →
- ∀U. ⇧*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #(↑i) :[h,a] U.
+ â\88\80T,i. â\9d¨G,Kâ\9d© ⊢ #i :[h,a] T →
+ ∀U. ⇧[1] T ≘ U → ❨G,K.ⓘ[I]❩ ⊢ #(↑i) :[h,a] U.
#h #a #I #G #K #T #i #H #U #HTU
elim (cnv_inv_cast … H) -H #X #HT #Hi #HTX #H2
-lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ{I}) … HTU) -HT
+lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ[I]) … HTU) -HT
[ /3 width=3 by drops_refl, drops_drop/ ] #HU
-lapply (cnv_lifts â\80¦ Hi (â\93\89) (ð\9d\90\94â\9d´1â\9dµ) (K.â\93\98{I}) ???) -Hi
+lapply (cnv_lifts â\80¦ Hi (â\93\89) (ð\9d\90\94â\9d¨1â\9d©) (K.â\93\98[I]) ???) -Hi
[4:|*: /3 width=3 by drops_refl, drops_drop/ ] #Hi
-elim (cpms_lifts_sn … HTX … (Ⓣ) … (K.ⓘ{I}) … HTU) -T
+elim (cpms_lifts_sn … HTX … (Ⓣ) … (K.ⓘ[I]) … HTU) -T
[| /3 width=3 by drops_refl, drops_drop/ ] #XU #HXU #HUXU
/3 width=5 by cnv_cast, cpms_lref/
qed.
(* Basic_1: was by definition: ty3_abbr *)
(* Basic_2A1: was by definition: nta_ldef ntaa_ldef *)
lemma nta_ldef_drops (h) (a) (G) (K) (L) (i):
- â\88\80V,W. â¦\83G,Kâ¦\84 ⊢ V :[h,a] W →
- ∀U. ⇧*[↑i] W ≘ U → ⇩*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[h,a] U.
+ â\88\80V,W. â\9d¨G,Kâ\9d© ⊢ V :[h,a] W →
+ ∀U. ⇧[↑i] W ≘ U → ⇩[i] L ≘ K.ⓓV → ❨G,L❩ ⊢ #i :[h,a] U.
#h #a #G #K #L #i #V #W #HVW #U #HWU #HLK
-elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d´1â\9dµ) (ð\9d\90\94â\9d´iâ\9dµ)) [| // ] #X #HWX #HXU
+elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d¨1â\9d©) (ð\9d\90\94â\9d¨iâ\9d©)) [| // ] #X #HWX #HXU
/3 width=9 by nta_lifts_bi, nta_ldef/
qed.
lemma nta_ldec_drops_cnv (h) (a) (G) (K) (L) (i):
- â\88\80W. â¦\83G,Kâ¦\84 ⊢ W ![h,a] →
- ∀U. ⇧*[↑i] W ≘ U → ⇩*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i :[h,a] U.
+ â\88\80W. â\9d¨G,Kâ\9d© ⊢ W ![h,a] →
+ ∀U. ⇧[↑i] W ≘ U → ⇩[i] L ≘ K.ⓛW → ❨G,L❩ ⊢ #i :[h,a] U.
#h #a #G #K #L #i #W #HW #U #HWU #HLK
-elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d´1â\9dµ) (ð\9d\90\94â\9d´iâ\9dµ)) [| // ] #X #HWX #HXU
+elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d¨1â\9d©) (ð\9d\90\94â\9d¨iâ\9d©)) [| // ] #X #HWX #HXU
/3 width=9 by nta_lifts_bi, nta_ldec_cnv/
qed.