Library additions.Wf_transparent

Transparent versions of wf_incl and wf_inverse_image

From Coq Require Export Relation_Definitions.

Lemma wf_incl_transparent :
∀ (A : Type) (R1 R2 : A → A → Prop),
Relation_Definitions.inclusion A R1 R2 → well_founded R2 → well_founded R1.

Section Inverse_Image_transp.
  Variables A B : Type.
  Variable R : B → B → Prop.
  Variable f : A → B.

  Let Rof (x y:A) : Prop := R (f x) (f y).

  Remark Acc_lemma : ∀ y:B, Acc R y → ∀ x:A, y = f x → Acc Rof x.

  Lemma Acc_inverse_image : ∀ x:A, Acc R (f x) → Acc Rof x.

  Theorem wf_inverse_image_transparent : well_founded R → well_founded Rof.

End Inverse_Image_transp.