-qed.
-
-lemma snv_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊩ #i :[g] →
- ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g].
-/2 width=3/ 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
-[ #L #k #a #I #V #T #H destruct
-| #I0 #L #K #V0 #i #_ #_ #a #I #V #T #H destruct
-| #b #I0 #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1/
-| #b #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct
-| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #a #I #V #T #H destruct
+qed-.
+
+lemma snv_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] →
+ ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
+/2 width=3 by snv_inv_lref_aux/ qed-.
+
+fact snv_inv_gref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥.
+#h #g #G #L #X * -G -L -X
+[ #G #L #k #p #H destruct
+| #I #G #L #K #V #i #_ #_ #p #H destruct
+| #a #I #G #L #V #T #_ #_ #p #H destruct
+| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #p #H destruct
+| #G #L #W #T #U #l #_ #_ #_ #_ #_ #p #H destruct
+]
+qed-.
+
+lemma snv_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ §p ¡[h, g] → ⊥.
+/2 width=8 by snv_inv_gref_aux/ qed-.
+
+fact snv_inv_bind_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
+ ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g].
+#h #g #G #L #X * -G -L -X
+[ #G #L #k #a #I #V #T #H destruct
+| #I0 #G #L #K #V0 #i #_ #_ #a #I #V #T #H destruct
+| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1 by conj/
+| #b #G #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_#_ #_ #a #I #V #T #H destruct
+| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct