proposition: Lemma wf_measure : forall f, wf (measure f).
proof: Proof. Proof using. intros f a. gen_eq n: (f a). gen a. pattern n. apply peano_induction. clear n. introv IH Eq. apply Acc_intro. introv H. unfolds in H. rewrite <- Eq in H. apply* IH. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)