-(* Advanced inversion lemmas ***********************************************)
-(*
-lemma frees_inv_zero_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≡ f →
- ∃∃g. K ⊢ 𝐅*⦃V⦄ ≡ g & f = ⫯g.
-#f #I #K #V #H elim (frees_inv_zero … H) -H *
-[ #H destruct
-| #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
-| #g #Z #Y #_ #H destruct
-]
-qed-.
-
-lemma frees_inv_zero_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≡ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯g.
-#f #I #K #H elim (frees_inv_zero … H) -H *
-[ #H destruct
-| #g #Z #Y #X #_ #H destruct
-| /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma frees_inv_lref_bind: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
- ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
-#f #I #K #i #H elim (frees_inv_lref … H) -H *
-[ #H destruct
-| #g #Z #Y #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
-]
-qed-.
-*)