lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ⫱f.
// qed.
-lemma tl_push_rew: â\88\80f. f = ⫱â\86\91f.
+lemma tl_push_rew: â\88\80f. f = ⫱⫯f.
#f <tl_rew <iota_push //
qed.
-lemma tl_next_rew: â\88\80f. f = ⫱⫯f.
+lemma tl_next_rew: â\88\80f. f = ⫱â\86\91f.
#f <tl_rew <iota_next //
qed.
-lemma tl_eq_repl: eq_repl â\80¦ (λf1,f2. ⫱f1 â\89\97 ⫱f2).
+lemma tl_eq_repl: eq_repl â\80¦ (λf1,f2. ⫱f1 â\89¡ ⫱f2).
#f1 #f2 * -f1 -f2 //
qed.