[ O ⇒ f | S m ⇒ ⫱(tls f m) ].
interpretation "tls (rtmap)" 'DropPreds n f = (tls f n).
(* Basic properties *********************************************************)
[ O ⇒ f | S m ⇒ ⫱(tls f m) ].
interpretation "tls (rtmap)" 'DropPreds n f = (tls f n).
(* Basic properties *********************************************************)