proposition: Theorem measure_rect_fix x : measure_rect x = @F x (fun y _ => measure_rect y).
proof: Proof. Proof using F_ext. unfold measure_rect; rewrite Fix_F_fix. apply F_ext. intros; apply Fix_F_Acc_irr. Qed.
imports: Arith Lia Wellfounded List Extraction Undecidability.Shared.Libs.DLW.Wf(acc_irr)