proposition: Lemma rel_incl_lexico2 : forall A1 A2 (R1 R1':binary A1) (R2 R2':binary A2), rel_incl R1 R1' -> rel_incl R2 R2' -> rel_incl (lexico2 R1 R2) (lexico2 R1' R2').
proof: Proof. Proof using. introv I1 I2. intros [x1 x2] [y1 y2] [H1|[H1 H2]]. { left~. } { subst. right~. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)