proposition: Lemma tele_map_app {T U} {TT : tele} (F : T → U) (t : TT -t> T) (x : TT) : (tele_map F t) x = F (t x).
proof: Proof. induction TT as [|X f IH]; simpl in *. - rewrite (tele_arg_O_inv x). done. - destruct (tele_arg_S_inv x) as [x' [a' ->]]. simpl. rewrite <-IH. done. Qed.
imports: stdpp(base tactics) stdpp(options)