Goal "s ~V~ t ==> (s > V) = (t > V)" ; by (rtac ext 1) ; by (rewrite_goals_tac [eq_u_def, ss_def]) ; by (case_tac "x : V" 1) ; by (Asm_simp_tac 1) ; by (Asm_simp_tac 1) ;