To prove individual derivations coinductively, one can use d: ... by coinduction...
Basic coinduction should be a nice addition to SASyLF: Coinductive rules: t1 ⇑ =======...
An easy way forward is to not complain about the lack of an assumption rule for a...
So it would be nice to define different kinds of contexts: Gamma one-variable-and-no-nonterminals...
Currently in SASyLF, the form of contexts is Gamma ::= only-terminals | Gamma one-variable-and-other-normal-nonterminals...
do case analysis on ... end case analysis is implemented. This new syntax doesn't...
use induction on x, {y, z} implemented. {x, y} means that one of x and y, in either...
The @ syntax is appealing for parsing purposes, but doesn't fit the original style...