proposition: Lemma wf_projected `{R1 : relation A} `(R2 : relation B) (f : A → B) : (∀ x y, R1 x y → R2 (f x) (f y)) → well_founded R2 → well_founded R1.
proof: Proof. intros Hf Hwf. cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R1 x). { intros aux x. apply (aux (f x)); auto. } induction 1 as [y _ IH]. intros x ?. subst. constructor. intros y ?. apply (IH (f y)); auto. Qed.
imports: stdpp(base) stdpp(options)