allow quantification over any tyvar in the environment, not just the first
add crude support for flattening with LetRec and Case at level zero
add support for flattening recursive-let
remove RLet and RWhere
let RCut take a left environment as well
remove RJoin rule
add RCut, RLeft, RRight rules
rename constructors of Arrange to start with A instead of R
move Arrange into NaturalDeductionContext
HaskProof: make the succedent level part of the judgment
add new Where rule, eliminate unnecessary ga_swaps in the Skolemizer
more efficient encoding of function types
integrate skolemization pass with flattening
first draft of skolemization pass