law eta_nn

lawful-fields@0.1.1.0 · proof_digits.bend:240

import Base

240law eta_nn:
241  for p: Nat & Nat
242  {p == (Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p)) : Nat & Nat}