lemma tls_O: ∀f. f = ⫱*[0] f.
// qed.
-lemma tls_S: â\88\80f,n. ⫱ ⫱*[n] f = ⫱*[⫯n] f.
+lemma tls_S: â\88\80f,n. ⫱ ⫱*[n] f = ⫱*[â\86\91n] f.
// qed.
-lemma tls_eq_repl: â\88\80n. eq_repl (λf1,f2. ⫱*[n] f1 â\89\97 ⫱*[n] f2).
+lemma tls_eq_repl: â\88\80n. eq_repl (λf1,f2. ⫱*[n] f1 â\89¡ ⫱*[n] f2).
#n elim n -n /3 width=1 by tl_eq_repl/
qed.
(* Advanced properties ******************************************************)
-lemma tls_xn: â\88\80n,f. ⫱*[n] ⫱f = ⫱*[⫯n] f.
+lemma tls_xn: â\88\80n,f. ⫱*[n] ⫱f = ⫱*[â\86\91n] f.
#n elim n -n //
qed.
(* Properties with pushs ****************************************************)
-lemma tls_pushs: â\88\80n,f. f = ⫱*[n] â\86\91*[n] f.
+lemma tls_pushs: â\88\80n,f. f = ⫱*[n] ⫯*[n] f.
#n elim n -n //
#n #IH #f <tls_xn //
qed.