Theorem: squashImplies (NazgandLean4/Prop.lean)

State before:
q r : Prop
⊢ q → q → r ↔ q → r
Tactic:
tauto
State after:
no goals