"context-sensitive exclusion from free variables (term)"
'CoFreeStar L i d T = (cofrees d i L T).
+(* Basic forward lemmas *****************************************************)
+
+lemma cofrees_fwd_lift: āL,U,d,i. L ā¢ i ~Ļµ š
*[d]ā¦Uā¦ ā āT. ā§[i, 1] T ā” U.
+/2 width=1 by/ qed-.
+
+lemma cofrees_fwd_bind_sn: āa,I,L,W,U,i,d. L ā¢ i ~Ļµ š
*[d]ā¦ā{a,I}W.Uā¦ ā
+ L ā¢ i ~Ļµ š
*[d]ā¦Wā¦.
+#a #I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ā{a,I}W2.U)) /2 width=1 by cpys_bind/ -W1
+#X #H elim (lift_inv_bind2 ā¦ H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_bind_dx: āa,I,L,W,U,i,d. L ā¢ i ~Ļµ š
*[d]ā¦ā{a,I}W.Uā¦ ā
+ L.ā{I}W ā¢ i+1 ~Ļµ š
*[ā«Æd]ā¦Uā¦.
+#a #I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ā{a,I}W.U2)) /2 width=1 by cpys_bind/ -U1
+#X #H elim (lift_inv_bind2 ā¦ H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_flat_sn: āI,L,W,U,i,d. L ā¢ i ~Ļµ š
*[d]ā¦ā{I}W.Uā¦ ā
+ L ā¢ i ~Ļµ š
*[d]ā¦Wā¦.
+#I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ā{I}W2.U)) /2 width=1 by cpys_flat/ -W1
+#X #H elim (lift_inv_flat2 ā¦ H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_flat_dx: āI,L,W,U,i,d. L ā¢ i ~Ļµ š
*[d]ā¦ā{I}W.Uā¦ ā
+ L ā¢ i ~Ļµ š
*[d]ā¦Uā¦.
+#I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ā{I}W.U2)) /2 width=1 by cpys_flat/ -U1
+#X #H elim (lift_inv_flat2 ā¦ H) -H /2 width=2 by ex_intro/
+qed-.
+
(* Basic inversion lemmas ***************************************************)
lemma cofrees_inv_gen: āL,U,U0,d,i. ā¦ā, Lā¦ ā¢ U ā¶*[d, ā] U0 ā (āT. ā§[i, 1] T ā” U0 ā ā„) ā
#X #H elim (lift_inv_lref2_be ā¦ H) -H //
qed-.
-(* Basic forward lemmas *****************************************************)
+lemma cofrees_inv_bind: āa,I,L,W,U,i,d. L ā¢ i ~Ļµ š
*[d]ā¦ā{a,I}W.Uā¦ ā
+ L ā¢ i ~Ļµ š
*[d]ā¦Wā¦ ā§ L.ā{I}W ā¢ i+1 ~Ļµ š
*[ā«Æd]ā¦Uā¦.
+/3 width=8 by cofrees_fwd_bind_sn, cofrees_fwd_bind_dx, conj/ qed-.
-lemma cofrees_fwd_lift: āL,U,d,i. L ā¢ i ~Ļµ š
*[d]ā¦Uā¦ ā āT. ā§[i, 1] T ā” U.
-/2 width=1 by/ qed-.
-
-lemma cofrees_fwd_nlift: āL,U,d,i. (āT. ā§[i, 1] T ā” U ā ā„) ā (L ā¢ i ~Ļµ š
*[d]ā¦Uā¦ ā ā„).
-#L #U #d #i #HnTU #H elim (cofrees_fwd_lift ā¦ H) -H /2 width=2 by/
-qed-.
+lemma cofrees_inv_flat: āI,L,W,U,i,d. L ā¢ i ~Ļµ š
*[d]ā¦ā{I}W.Uā¦ ā
+ L ā¢ i ~Ļµ š
*[d]ā¦Wā¦ ā§ L ā¢ i ~Ļµ š
*[d]ā¦Uā¦.
+/3 width=7 by cofrees_fwd_flat_sn, cofrees_fwd_flat_dx, conj/ qed-.
(* Basic Properties *********************************************************)