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

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

State before:
A : Prop
h : A
⊢ A = True
Tactic:
exact propext (Iff.intro (λ _ => True.intro) (λ _ => h))
State after:
no goals