/3 width=1 by lex_bind, ext2_unit/ qed.
(* Basic_2A1: was: lpx_sn_pair *)
lemma lex_pair (R): ∀I,K1,K2,V1,V2. K1 ⪤[R] K2 → R K1 V1 V2 →
/3 width=1 by lex_bind, ext2_unit/ qed.
(* Basic_2A1: was: lpx_sn_pair *)
lemma lex_pair (R): ∀I,K1,K2,V1,V2. K1 ⪤[R] K2 → R K1 V1 V2 →