lean4-logic
lean4-logic copied to clipboard
Definability of `.𝟑`
.𝟑 is not Geach axiom and its definability is functional.