Theorem: LoVe.not_ServAhead_advRecv (LoVe/Labs/Lab5Solution.lean)

State before:
⊢ ¬ServAhead Score.advRecv
Tactic:
intro h
State after:
h : ServAhead Score.advRecv
⊢ False

State before:
h : ServAhead Score.advRecv
⊢ False
Tactic:
cases h
State after:
no goals