pub fn initialize_full<K, V, Pred: InvariantPredicate<K, V>>(
    post: State<K, V, Pred>,
    k: K,
    t: V
)