Theorem: t (Katydid/Std/Tipe.lean)

State before:
⊢ 1 ≡ 2 → False
Tactic:
intro x
State after:
x : 1 ≡ 2
⊢ False

State before:
x : 1 ≡ 2
⊢ False
Tactic:
contradiction
State after:
no goals