fact: Definition lexico4 {A1 A2 A3 A4} (R1:binary A1) (R2:binary A2) (R3:binary A3) (R4:binary A4) : binary (A1*A2*A3*A4) := lexico2 (lexico3 R1 R2 R3) R4.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)