def pair_snd

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/logic.bend:98

import Base

98def pair_snd(-A: Type, -B: Type, a: A, b: B, c: A, d: B, e: {(a, b) == (c, d) : A & B}) -> {b == d : B}:
99  Equal.cong(A & B, B, p => Pair.snd(A, B, p), (a, b), (c, d), e)