[X->A,y->B](y)=B           [X->A,y->B](y)=B
                    ------------------------    ------------------------
                    C,[X->A,y->B],X,σ |- y:B    C,[X->A,y->B],X,σ |- y:B   B |- A foo(B) ∅ 
                    ----------------------------------------------------------------------
[X->A,y->B](x)=A                            C,[X->A,y->B],X,σ |- y.foo(y): A                    A:=A
----------------------------------------------------------------------------------------------------
                                           C,[X->A,y->B],X,σ |- x=y.foo(y): A
                                           ----------------------------------
                                            C,[X->A,y->B],X,σ |- x=y.foo(y);
                                           ----------------------------------
                                           C,[x->A],X,σ |- {B y; x=y.foo(y);}
                                         -------------------------------------
                                         C,[],X,σ |- {A x; {B y; x=y.foo(y);}}