Palalansoukî
Results
2
comments of
Palalansoukî
HilbertStyleの補題を使っている証明をhttps://github.com/iehality/lean4-logic/blob/master/Logic/AutoProver/Prover.lean の`by prover [ ... ]`タクティックで置き換えられないだろうか？
`LO.Propositional.Classical`と`LO.FirstOrder`の移行完了しました