(* *)
(**************************************************************************)
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/xprs.ma".
+include "basic_2/computation/dxprs.ma".
include "basic_2/equivalence/cpcs.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
| snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T)
| snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T →
⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
- ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
+ ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T)
.
∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g].
/2 width=3/ qed-.
+fact snv_inv_gref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀p. X = §p → ⊥.
+#h #g #L #X * -L -X
+[ #L #k #p #H destruct
+| #I #L #K #V #i #_ #_ #p #H destruct
+| #a #I #L #V #T #_ #_ #p #H destruct
+| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #p #H destruct
+| #L #W #T #U #l #_ #_ #_ #_ #p #H destruct
+]
+qed.
+
+lemma snv_inv_gref: ∀h,g,L,p. ⦃h, L⦄ ⊩ §p :[g] → ⊥.
+/2 width=7/ qed-.
+
fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g].
#h #g #L #X * -L -X
fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T →
∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
- ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U.
+ ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
#h #g #L #X * -L -X
[ #L #k #V #T #H destruct
| #I #L #K #V0 #i #_ #_ #V #T #H destruct
lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] →
∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
- ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U.
+ ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
/2 width=3/ qed-.
fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T →