How to add an element to a total function while making sure no other mapping to this element exists?

I am trying to formally specify a railway interlocking system with the B method in Atelier B. The most basic underlying concept is very simple: trains can be assigned a location and an area. There can only be one train in one area at the same time. The area is just a set of locations, defined as a total function of a train element mapped to a powerset of the location set: train_areas : trains --> POW(LOCATION). To make sure no location is mapped to two trains, one invariant should be something akin to

!(t1, t2). (t1 : trains & t2 : trains => train_areas(t1) /\ train_areas(t2) = {})

For every two trains, the intersection of the sets of locations which the trains map to in train_areas should be an empty set. I have also tried expressing it like so:

!(locs1, locs2).(locs1 : ran(train_areas) & locs2 : ran(train_areas) & locs1 /= locs2 => locs1 /\ locs2 = {})

For every two sets of locations included in the range of the train_areas variable - that are not the same - the intersection of the locations should be an empty set. It can also be expressed like so:

!tt. (tt : trains => train_areas(tt) /\ union(ran(train_areas) - {train_areas(tt)}) = {})

For all train elements, the intersection of the locations mapped to the train in train_areas and the range of the locations mapped to in train_areas minus the locations mapped to the train in question should be an empty set.

Now I want to add a train. The train needs to have it's own location and the location of course needs to be included in a set of locations which the train is mapped to in train_areas. I am making sure the location is not already included in the train_areas set like so:

!train.(train : trains => {loc} /\ train_areas(train) = {})

For all train elements, the intersection of the newly added location and the locations already mapped to from the train in train_areas is an empty set. I have also added this condition in every other way I could think of to express it. Despite everything, the invariants mentioned above can not be proven to hold by Atelier B when adding a new mapping to the train_areas variable like so train_areas := train_areas \/ {tt |-> {loc}} (Union of everything in train_areas and the new train with its powerset of locations).

For some reason, even though it was checked multiple times that the new train location loc is not present in train_areas, after adding {tt |-> {loc}} to train_areas, it cannot be proven that no two trains are mapped to same location in train_areas. Can someone help me to understand Atelier B better and express this very simple problem? Please find the full machine down below:

MACHINE APSTrackside
SETS
    AREA ; LOCATION ; TRAIN    
VARIABLES
    areas, train_locations, trains, train_areas
INVARIANT
    trains <: TRAIN &
    
    // Every train area is associated with a set of locations
    train_areas : trains --> POW(LOCATION) &

    // Every area is associated with a set of locations
    areas : AREA --> POW(LOCATION) &
    
    // Every train is associated with a location
    train_locations : trains --> LOCATION &
    
    // Every train needs to be assigned a set of locations in train_areas
    !tt.(tt : trains => train_locations(tt) : train_areas(tt)) &
    
    // There can only be one train in any one area at the same time
    // Here is the problem    
    !(locs1, locs2).(locs1 : ran(train_areas) & locs2 : ran(train_areas) & locs1 /= locs2 
        => locs1 /\ locs2 = {})
    
INITIALISATION
    trains := {} ||
    train_locations := {} ||
    train_areas := {} ||
    areas := %area.(area : AREA | {ll | ll:LOCATION})
    
OPERATIONS    
    AddTrain(tt, loc) =
    PRE
        tt : TRAIN &
        loc : LOCATION &
        tt /: trains &
        
        // The location is not in any currently set up train area
        !train.(train : trains => {loc} /\ train_areas(train) = {}) &
        !locs.(locs : ran(train_areas) => loc /: locs) &
        loc /: union(ran(train_areas)) &
        
        // Ensure the location is not already occupied by any train
        !train.(train : dom(train_areas) => loc /: train_areas(train)) &
        
        // Ensure the new train's location doesn't overlap with any existing train's area
        !(tt1).(tt1 : trains => loc /: train_areas(tt1)) &
        
        // There is no other train at this location
        !tt.(tt : trains => loc /= train_locations(tt))
    THEN
        trains := trains \/ {tt} ||
        train_locations := train_locations \/ {tt |-> loc} ||
        // Here is the problem
        train_areas := train_areas \/ {tt |-> {loc}}
    END
END

The new term is being substituted into the invariant like so:

tt1 : trains \/ {tt} 
=>
(train_areas \/ {tt |-> {loc}})(tt1) /\ 
union(ran(train_areas \/ {tt |-> {loc}}) 
-s ({(train_areas \/ {tt |-> {loc}})(tt1)})) = {}

I managed to solve the problem by using the interactive prover of Atelier B. The logic was correct, but for reasons I don't understand yet, it couldn't be processed by the automatic prover.

The interactive prover allows to rearrange the prove obligation until it can be proven (by clicking "Prove" multiple times, no other steps are required). It is also possible to add the precondition as a new hypothesis and to prove the obligation with respect to the new hypothesis.