proposition: Lemma wf_lexico2 : forall A1 A2 (R1:binary A1) (R2:binary A2), wf R1 -> wf R2 -> wf (lexico2 R1 R2).
proof: Proof. Proof using. introv W1 W2. intros [x1 x2]. gen x2. induction_wf IH1: W1 x1. intros. induction_wf IH2: W2 x2. constructor. intros [y1 y2] H. simpls. destruct H as [H1|[H1 H2]]. apply~ IH1. rewrite H1. apply~ IH2. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)