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

State before:
p : Prop
⊢ (True → p) → p
Tactic:
intro htp
State after:
p : Prop
htp : True → p
⊢ p

State before:
p : Prop
htp : True → p
⊢ p
Tactic:
exact htp trivial
State after:
no goals