(* Destructions with cpp ****************************************************)
-lemma tls_plus_lift_rmap_closed (f) (q) (n):
- q Ļµ šāØnā© ā
+lemma tls_plus_lift_rmap_closed (o) (f) (q) (n):
+ q Ļµ šāØo,nā© ā
ām. ā*[m]f ā ā*[m+n]ā[q]f.
-#f #q #n #Hq elim Hq -q -n //
+#o #f #q #n #Hq elim Hq -q -n //
#q #n #_ #IH #m
<nplus_succ_dx <stream_tls_swap //
qed-.
-lemma tls_lift_rmap_closed (f) (q) (n):
- q Ļµ šāØnā© ā
+lemma tls_lift_rmap_closed (o) (f) (q) (n):
+ q Ļµ šāØo,nā© ā
f ā ā*[n]ā[q]f.
-#f #q #n #H0
-/2 width=1 by tls_plus_lift_rmap_closed/
+#o #f #q #n #H0
+/2 width=2 by tls_plus_lift_rmap_closed/
qed-.
-lemma tls_succ_lift_rmap_append_L_closed_dx (f) (p) (q) (n):
- q Ļµ šāØnā© ā
+lemma tls_succ_lift_rmap_append_L_closed_dx (o) (f) (p) (q) (n):
+ q Ļµ šāØo,nā© ā
ā[p]f ā ā*[ān]ā[pāšāq]f.
-#f #p #q #n #Hq
-/3 width=1 by tls_lift_rmap_closed, pcc_L_sn/
+#o #f #p #q #n #Hq
+/3 width=2 by tls_lift_rmap_closed, pcc_L_sn/
qed-.