Lemma 51 ([The two pairing laws]). Under h:Resp(v) , let P_x=Pair(Part(v),x⁰) . For every x':X there are proofs P_x@(x'^ \,ℓ ), ↔ v_m(x'^ \,0 ), ; P_x@(x'^ \,r ), ↔x≃x'.

For forward, first negate T_r(x^0,x'^ \,ℓ ) . Given such a proof, map it forward through Lemma 50 ([Class and edge witnesses]) and open its witness u into . Its second conjunct is x'^ \,ℓ ∼u^r , contradicted by diff_ ℓ,r . Given p:P_x@(x'^ \,ℓ ) , use pv and this negation to extract ∃y.\, (T_ℓ(y,x'^ \,ℓ )(v)@y). Open it as y,q , and open the edge witness from the first conjunct as u,q_0,q_ℓ , where q_0:y∼u^0, q_ℓ:x'^ \,ℓ ∼u^ℓ. The proof TagBack_ℓ(q_ℓ) is x'≃u . Symmetrize it and apply Tag_0 , then compose with q_0 , to get e:y∼x'^ \,0 . From the second conjunct of q , the unrounded Part evaluation gives v_m y . Apply h[y][x'^ \,0 ]·e forward to obtain the target v_m(x'^ \,0 ) . Each opening uses this fixed target. For the left reverse implication, a proof of v_m(x'^ \,0 ) gives Part(v)@(x'^ \,0 ) by backward. Witness x' with the two reflexivities in the edge equivalence backward to get T_ℓ(x'^ \,0 ,x'^ \,ℓ ) . Pair these, witness y=x'^ \,0 , inject the resulting existential into form , and apply pv backward. For forward, negate ∃y.(T_ℓ(y,x'^ \,r )(v)@y) . Open an assumed existential into , open its T_ℓ witness, and contradict its second conjunct x'^ \,r ∼u^ℓ with diff_ r,ℓ . Thus pv maps a proof of P_x@(x'^ \,r ) to T_r(x^0,x'^ \,r ) . Open its witness u , with x^0∼u^0 and x'^ \,r ∼u^r . The two same-tag converses give x≃u and x'≃u . Compose the first with the symmetry of the second to prove x≃x' . For the reverse, given e:x≃x' , witness x in the edge equivalence with reflexivity at x^0 and Tag_r(sym(e)): x'^ \,r ∼x^r . This gives T_r(x^0,x'^ \,r ) ; inject it into form , then apply pv backward. Abstract each input proof and pair the two directions.