For that we need a slightly stronger property for distributing a later over an existential quantifier.