Constraint: Designing a complex constraints which involve a check over exitsence

[hfaghihi15]

I want to make a constraint to describe the following dependency:

If entity 'e' is located in a location 'l', which corresponds to an entity 'e1' and entity 'e1' is destroyed, the entity `e` is either moved or destroyed

This means the following example: 
if `bone` is located in `body`, the `body` is destroyed at step `i`, then `bone` is either moved or destroyed at step `i`. 

To help with designing this constraint, I have an additional concept named same_mention which connects the locations and entities which refer to the same object.

I have prepared the following but my concern is the connection made from existsL and the conditions coming after the andL or outside of the existsL. I am not sure if those connections would be properly made.

### if entity 'e' is located in a location 'l' which corresponds to an entity 'e' and entity 'e' is destroyed, the entity is either moved or destroyed
    forAllL(
        combinationC(step, entity)('i', 'e'),
        ifL(
            andL(
                entity_location_label('el1', path=(
                                ("e", lentity.reversed),
                                ("i", lstep.reversed)
                )),
                existsL(
                    same_mention('sm1', path=(
                        ("el1", llocation, same_location.reversed)
                    ))
                ),
                action_destroy('a1', path=(
                    ("sm1", same_entity, action_entity.reversed),
                    ("i", action_step.reversed)
                ))
            ),
            orL(
                action_move('a2', path=(
                    ("e", action_entity.reversed),
                    ("i", action_step.reversed)
                )),
                action_destroy('a3', path=(
                    ("e", action_entity.reversed),
                    ("i", action_step.reversed)
                ))
            )
        )
    )

[hfaghihi15]

I can also change the existsL constraint to the following which makes more sense to me. But it would be great if you could elaborate on the differences of the implications:

existsL(
                    andL(
                        same_mention('sm1', path=(
                        ("el1", llocation, same_location.reversed)
                        )),
                        action_destroy('a1', path=(
                            ("sm1", same_entity, action_entity.reversed),
                            ("i", action_step.reversed)
                        )),
                    ) 
                ),

[hfaghihi15]

The same issue maybe more sensible for the following constraint, where entangling the two conditions inside one existL is not possible.

### if the location of entity `e` is `l` which matches another entity `e1`, then the entity `e1` should exist
    forAllL(
        combinationC(step, entity)('i', 'e'),
        ifL(
            andL(
                entity_location_label('el1', path=(
                                ("e", lentity.reversed),
                                ("i", lstep.reversed)
                    )
                ),
                existsL(
                    same_mention('sm1', path=(
                        ("el1", llocation, same_location.reversed)
                    ))
                )
            ),
            after_existence('a1', path=(
                ("sm1", same_entity, action_entity.reversed),
                ("i", action_step.reversed)
            ))
        )
    )