proposition: Lemma wf_prod2_of_wf_1 : forall (A1 A2:Type) (R1:binary A1) (R2:binary A2), wf R1 -> wf (prod2 R1 R2).
proof: Proof. Proof using. introv W1. intros [x1 x2]. gen x2. induction_wf IH: W1 x1. intros. constructor. intros [y1 y2] [E1 E2]. apply~ IH. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)