class CRDT t where
  type Op t -- ^ the amount of operations you can use to update the data structure
  
  apply :: t -> Op t -> t -- ^ update using operations function
  
  lawCommut :: x:t -> op1:Op t -> op2:Op t -> { _:Proof | apply (apply x op1) op2 = apply (apply x op2) op1 }
  -- ^ we want commutativity preserved by CRDT
  -- so all operations actually form a **commutative monoid**
  -- it is a commutative monoid set / module.
  
strongConvergence :: (Eq (Op a), CRDT a) => s0:a -> ops1:[Op a] -> ops2:[Op a] -> {_:Proof | isPermutation ops1 ops2 => applyAll s0 ops1 = applyAll s0 ops2 }
-- this is obvious once you have lawCommut