-qed.
-
-lemma snv_inv_gref: ∀h,g,L,p. ⦃G, L⦄ ⊢ §p ¡[h, g] → ⊥.
-/2 width=7/ qed-.
-
-fact snv_inv_bind_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
- ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ T ¡[h, 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_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/
+| #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