Palalansoukî

system

1

close #22

(first-order / propositional) formulae are defined as Tait-style formula, and it is inconsistent with minimal logic, intuitionistic logic, etc. Perhaps we should modify the definition to that of an ordinary...

Currently, there is two different characterization of deduction system, `LO.System` and `LO.Deduction`, but they are redundant and should be unified.

Add framework for sequent calculi. ```lean class SequentCalc₁ {F : outParam Type*} (R : outParam Type*) [Precollection F R] (S : Type*) where Sqt : S → R → Type*...