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
migrate HaskStrong away from using LeveledHaskType
HaskProof: make the succedent level part of the judgment
rename variables to avoid Coq pickiness during extraction
add new Where rule, eliminate unnecessary ga_swaps in the Skolemizer
add an identity production for Arrange
swap order of hypotheses in RApp to match RLet
allow rank-1 polymorphic types for globals
prove all [admit]ted lemmas in HaskStrongToProof (not necessarily elegantly!)
remove ClosedSIND (use "SIND []" instead)
update to new coq-categories, base ND_Relation on inert sequences
formatting fixes