proposition: Lemma applyn_altern : forall A B (f : A -> B) (g : B -> A) x n, applyn n (fun x => f (g x)) (f x) = f (applyn n (fun x => g (f x)) x).
proof: Proof. Proof using. introv. gen x. induction~ n. introv. repeat rewrite applyn_fix. autos~. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)