include "ground_2/relocation/rtmap_sor.ma".
include "basic_2/notation/relations/freestar_3.ma".
-include "basic_2/grammar/lenv.ma".
+include "basic_2/syntax/lenv.ma".
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
/2 width=4 by frees_inv_flat_aux/ qed-.
+(* 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/
+]
+qed-.
+
+lemma frees_inv_lref_pair: ∀f,I,K,V,i. K.ⓑ{I}V ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
+ ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
+#f #I #K #V #i #H elim (frees_inv_lref … H) -H *
+[ #H destruct
+| #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
+]
+qed-.
+
(* Basic forward lemmas ****************************************************)
lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄.
/4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
qed.
-(* Basic_2A1: removed theorems 27:
+(* Basic_2A1: removed theorems 30:
frees_eq frees_be frees_inv
frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
frees_inv_bind frees_inv_flat frees_inv_bind_O
frees_lref_eq frees_lref_be frees_weak
frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
+ frees_lift_ge frees_inv_lift_be frees_inv_lift_ge
lreq_frees_trans frees_lreq_conf
llor_atom llor_skip llor_total
llor_tail_frees llor_tail_cofrees