I want to show that $\Vert \check x = \check y \Vert = 1$ implies $x = y$, where $\check x$ is the canonical name for $x$ in $V^B$.
I'd like try induction over the ranks of $\check x$ and $\check y$ and so far I have deduced that for every $t \in \operatorname{dom}(\check x): \sum_{s \in \operatorname{dom}(\check y)} \Vert s = t \Vert = 1$.
Here I is where I'm having difficulties. I'm unable show that there actually is an $s \in \operatorname{dom}(\check y)$ satisfying $\Vert s = t \Vert = 1$.
The fact that $V^B$ is full yields an $m \in V^B : \Vert s = t \Vert = 1$, so I guess I could try to go over the proof of the fullness of $V^B$ to determine, whether m is in $\operatorname{dom}(\check y)$ or not.
Should I do that or am I missing something much simpler?