Expressing dedicated resource

Stream: lean4

[Yasu Watanabe]

I'm trying to express some constraints about resources but I'm stuck.
My idea is to use dependent type as a constraint for resources non-transferrable.
It fail to achieve my intention.
I'd like to know a technic to solve the issue below. I wanted to prove, if I give a tool, the person has the tool but the type check of the statement failed with obvious reason.

import Mathlib

/- This is a bit artificial because this model is reduced version of my problem to solve.
The situation assumes:
  - A person has 0-2 tools dedicated to the person only.
  - The intention of the code below is to avoid accidental transfer tool to other person.
-/
def PersonId := Nat

-- Tool belong to someone specified by PersonalId and non transferable.
inductive Tool (person : PersonId) where
| pen
| paper

-- Person has his/her PersonalID and set of tools.
structure Person where
  pid : PersonId
  tool : Set (Tool pid) -- The intention of this is to model a Tool belong to someone by pid.

-- Initially, person don't have any tool.
def init_person (pid : Nat) : Person := ⟨ pid, {} ⟩

-- Give tool and it is bound to the eprson by pid.
def give_tool (p : Person) (r : Tool p.pid) : Person :=
  let ⟨ id, tool ⟩ := p
  let tool' := tool.insert r
  ⟨ id, tool' ⟩

/- I'd like to prove:
  for any Person p if I give any tool to him/her, tool box contain the tool given.

  r ∈ q.res does not type check because pid of r and q is not supposed to be same. -/
example : ∀ (p q : Person) (t : Tool p.pid) , q = give_tool p t → ¬ (t ∈ q.tool) := _