p1.l-8: [u] : Γ.A -> Γ ---> [u] : Γ -> Γ.A