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