proposition: Theorem measure_double_rect_paired x y : P x y.
proof: Proof. Proof using F. change (Q (x,y)). generalize (x,y); clear x y; intros c. induction on c as IH with measure (m' c). destruct c as (x,y); apply F. intros ? ?; apply (IH (_,_)). Defined.
imports: Arith Lia Wellfounded List Extraction Undecidability.Shared.Libs.DLW.Wf(acc_irr)