(* Advanced properties on native type assignment for terms ******************)
-lemma nta_pure_ntas: ∀h,L,U,W,Y. ⦃h, L⦄ ⊢ U :* ⓛW.Y → ∀T. ⦃h, L⦄ ⊢ T : U →
- ∀V. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.U.
+lemma nta_pure_ntas: ∀h,L,U,W,Y. ⦃h,L⦄ ⊢ U :* ⓛW.Y → ∀T. ⦃h,L⦄ ⊢ T : U →
+ ∀V. ⦃h,L⦄ ⊢ V : W → ⦃h,L⦄ ⊢ ⓐV.T : ⓐV.U.
#h #L #U #W #Y #H @(ntas_ind_dx … H) -U /2 width=1/ /3 width=2/
qed.
-axiom pippo: ∀h,L,T,W,Y. ⦃h, L⦄ ⊢ T :* ⓛW.Y → ∀U. ⦃h, L⦄ ⊢ T : U →
- ∃Z. ⦃h, L⦄ ⊢ U :* ⓛW.Z.
+axiom pippo: ∀h,L,T,W,Y. ⦃h,L⦄ ⊢ T :* ⓛW.Y → ∀U. ⦃h,L⦄ ⊢ T : U →
+ ∃Z. ⦃h,L⦄ ⊢ U :* ⓛW.Z.
(* REQUIRES SUBJECT CONVERSION
#h #L #T #W #Y #H @(ntas_ind_dx … H) -T
[ #U #HYU
(* Advanced inversion lemmas on native type assignment for terms ************)
-fact nta_inv_pure1_aux: ∀h,L,Z,U. ⦃h, L⦄ ⊢ Z : U → ∀X,Y. Z = ⓐY.X →
- ∃∃W,V,T. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V &
- L ⊢ ⓐY.V ⬌* U & ⦃h, L⦄ ⊢ V :* ⓛW.T.
+fact nta_inv_pure1_aux: ∀h,L,Z,U. ⦃h,L⦄ ⊢ Z : U → ∀X,Y. Z = ⓐY.X →
+ ∃∃W,V,T. ⦃h,L⦄ ⊢ Y : W & ⦃h,L⦄ ⊢ X : V &
+ L ⊢ ⓐY.V ⬌* U & ⦃h,L⦄ ⊢ V :* ⓛW.T.
#h #L #Z #U #H elim H -L -Z -U
[ #L #k #X #Y #H destruct
| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
qed.
(* Basic_1: was only: ty3_gen_appl *)
-lemma nta_inv_pure1: ∀h,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
- ∃∃W,V,T. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V &
- L ⊢ ⓐY.V ⬌* U & ⦃h, L⦄ ⊢ V :* ⓛW.T.
+lemma nta_inv_pure1: ∀h,L,Y,X,U. ⦃h,L⦄ ⊢ ⓐY.X : U →
+ ∃∃W,V,T. ⦃h,L⦄ ⊢ Y : W & ⦃h,L⦄ ⊢ X : V &
+ L ⊢ ⓐY.V ⬌* U & ⦃h,L⦄ ⊢ V :* ⓛW.T.
/2 width=3/ qed-.
-axiom nta_inv_appl1: ∀h,L,Z,Y,X,U. ⦃h, L⦄ ⊢ ⓐZ.ⓛY.X : U →
- ∃∃W. ⦃h, L⦄ ⊢ Z : Y & ⦃h, L⦄ ⊢ ⓛY.X : ⓛY.W &
+axiom nta_inv_appl1: ∀h,L,Z,Y,X,U. ⦃h,L⦄ ⊢ ⓐZ.ⓛY.X : U →
+ ∃∃W. ⦃h,L⦄ ⊢ Z : Y & ⦃h,L⦄ ⊢ ⓛY.X : ⓛY.W &
L ⊢ ⓐZ.ⓛY.W ⬌* U.
(* REQUIRES SUBJECT REDUCTION
#h #L #Z #Y #X #U #H