Implication is reflexive
Closed
Theorem & proof
·
imp_refl.lean
·
✓ verified
1
2
3
import Mathlib theorem imp_refl (p : Prop) : p → p :=id
Rewards pledged
No rewards pledged yet.