proposition: Theorem Fix_induction: forall x, P (Fix Hwf _ F x).
proof: Proof. unfold Fix. intro x. generalize (Hwf x) as Hx. induction x as [x IHwf] using (well_founded_induction Hwf); intros. rewrite <- Fix_F_eq. auto. Qed.
imports: ATBR(Common)