proposition: Lemma lexico4_3 : forall x1 x2 x3 x4 y1 y2 y3 y4, x1 = y1 -> x2 = y2 -> R3 x3 y3 -> lexico4 R1 R2 R3 R4 (x1,x2,x3,x4) (y1,y2,y3,y4).
proof: Proof. Proof using. intros. left. right~. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)