proposition: Lemma wf_measure2 : forall A1 A2 (f:A1->A2->nat), wf (measure2 f).
proof: Proof. Proof using. intros A1 A2 f [x1 x2]. apply (@measure_induction _ (uncurry2 f)). clear x1 x2. intros [x1 x2] H. apply Acc_intro. intros [y1 y2] Lt. apply~ H. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)