proposition: Lemma applyn_ind : forall A (P : A -> Prop) (f : A -> A) x n, (forall x, P x -> P (f x)) -> P x -> P (applyn n f x).
proof: Proof. Proof using. introv I. induction n; introv Hx; autos*. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)