6 lines
108 B
Lean4
6 lines
108 B
Lean4
import Game.Tactic.Rfl
|
|
|
|
/- Custom `rfl` should close `A ↔ A`. -/
|
|
example (A : Prop) : A ↔ A := by
|
|
rfl
|