Theorem: Smt.Reconstruct.Prop.trueElim (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ {A : Prop}, A = True → A
Tactic:
intros A h
State after:
A : Prop
h : A = True
⊢ A

State before:
A : Prop
h : A = True
⊢ A
Tactic:
rewrite [h]
State after:
A : Prop
h : A = True
⊢ True

State before:
A : Prop
h : A = True
⊢ True
Tactic:
trivial
State after:
no goals