proposition: Lemma wf_rel_preimage : forall A B (R:binary B) (f:A->B), wf R -> wf (rel_preimage R f).
proof: Proof. Proof using. introv W. intros x. gen_eq a: (f x). gen x. induction_wf IH: W a. introv E. constructors. intros y Hy. subst a. hnf in Hy. applys* IH. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)