proposition: Lemma Fix_unfold_rel `{R : relation A} (wfR : well_founded R) (B : A → Type) (E : ∀ x, relation (B x)) (F: ∀ x, (∀ y, R y x → B y) → B x) (HF: ∀ (x: A) (f g: ∀ y, R y x → B y), (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g)) (x: A) : E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)).
proof: Proof. unfold Fix. destruct (wfR x); simpl. apply HF; intros. apply Fix_F_proper; auto. Qed.
imports: stdpp(base) stdpp(options)