def pair_eta

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

import Base

122def pair_eta(-A: Type, -B: Type, p: A & B) -> {p == (Pair.fst(A, B, p), Pair.snd(A, B, p)) : A & B}:
123  match p:
124    case Tuple{a, b}:
125      {==}