proposition: Theorem rel_to_wf: well_founded R.
proof: Proof. intro a. remember (f a) as fa. revert a Heqfa. induction fa as [fa IHa] using (well_founded_induction HR). constructor. intros a' H. subst. eapply IHa; trivial. constructor. trivial. Qed.
imports: ATBR(Common)