~/jendhub

law none_some

lawful-bytes@0.1.1.0 · proof_same.bend:29

import lawful-bytes@0.1.1.0/proof_same.bend as ProofSame
import Base

29law none_some:
30  for -x: U32
31  for e: {None{} == Some{x} : Maybe<&2, U32>}
32  Empty

Uses (6)

Used by (2)