Theorem: Smt.Reconstruct.Prop.orFalse (Smt/Reconstruct/Prop/LiftOrNToNeg.lean)

State before:
⊢ ∀ {A : Prop}, A ∨ False → A
Tactic:
intros a h
State after:
a : Prop
h : a ∨ False
⊢ a

State before:
a : Prop
h : a ∨ False
⊢ a
Tactic:
cases h with
| inl ha => exact ha
| inr ff => exact False.elim ff
State after:
no goals

State before:
case inl
a : Prop
ha : a
⊢ a
Tactic:
exact ha
State after:
no goals

State before:
case inr
a : Prop
ff : False
⊢ a
Tactic:
exact False.elim ff
State after:
no goals