Palalansoukî comments

Results 3 comments of


                                            Palalansoukî

HilbertStyleの補題を使っている証明をhttps://github.com/iehality/lean4-logic/blob/master/Logic/AutoProver/Prover.lean の`by prover [ ... ]`タクティックで置き換えられないだろうか？

`LO.Propositional.Classical`と`LO.FirstOrder`の移行完了しました

> ```lean > abbrev FrameClassOfSystem (α : Type u) {S : Type u} [System (Formula α) S] (𝓢 : S) : FrameClass.Dep α := { (F : Frame.Dep α) |...