proposition: Lemma tele_fun_compose_eq {TT1 TT2 TT3 : tele} (f : TT2 -t> TT3) (g : TT1 -t> TT2) x : tele_fun_compose f g $ x = (f ∘ g) x.
proof: Proof. unfold tele_fun_compose. rewrite tele_app_bind. done. Qed.
imports: stdpp(base tactics) stdpp(options)