proposition: Theorem rel_of_wf: well_founded rel_of.
proof: Proof. unfold rel_of. 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. eauto. Qed.
imports: ATBR(Common)