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