take (0). V ; :: thesis: ( (0). V is strict & (0). V is free )
thus ( (0). V is strict & (0). V is free ) ; :: thesis: verum