proposition: Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x : (tele_bind f) x = f x.
proof: Proof. induction TT as [|X b 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)