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