Theorem: trueImpliesOnlyTrue (NazgandLean4/Prop.lean)

State before:
p r : Prop
⊢ p → (p → r ↔ r)
Tactic:
tauto
State after:
no goals