Modeling hypothetical judgments

The meaning of $x \in A \vdash b \in B$ is that A is a type and for any two elements, a, a' of A, B[a/x] is a type and B[a/x]=B[a'/x] (i.e. B is type functional in A), and moreover, $b[a/x] \in B[a/x]$ and b[a/x]=b[a'/x] in B[a/x]. We have extended this notion to multiple hypotheses inductively to define $x_1 \in A_1, \ldots, x_n \in A_n \vdash b \in B$. This definition can be carried over to type systems.