def wd.eta

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:146

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

146# a pair is its two parts
147def wd.eta(p: W.W64 & W.W64) -> {p == (W.W64.fst(p), W.W64.snd(p)) : W.W64 & W.W64}:
148  (q, r) = p
149  {==}