+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-.
+