assert AllGoodAlg = ∀ alg . GoodAlg alg property GoodAlg = {| alg | ∀ ws . ∀ regf . StateIndependent {doPacket alg ws regf} |} property StateIndependent = {| m | ∀ s1 . ∀ s2 . {fst (runS m s1)} === {fst (runS m s2)} |}