proposition: Lemma applyn_comp : forall A n m f (x : A), applyn n f (applyn m f x) = applyn (n + m) f x.
proof: Proof. Proof using. introv. gen m; induction n; introv; simpls~. rewrite~ IHn. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)