Theorem: Yb_ne_Yc (FM2023Exrcise/section03_functions/sheet3.lean)

State before:
⊢ Y.b ≠ Y.c
Tactic:
intro h
State after:
h : Y.b = Y.c
⊢ False

State before:
h : Y.b = Y.c
⊢ False
Tactic:
cases h
State after:
no goals