The inner constructor of the DerivationTree accepts PreDerivationTrees as children instead of directly expecting DerivationTrees. The latter seems more natural to me. In #28 the induction principle is already reworked and once the inner constructor is changed, the induction principle (recOn') can likely be further improved.
The
innerconstructor of theDerivationTreeacceptsPreDerivationTrees as children instead of directly expectingDerivationTrees. The latter seems more natural to me. In #28 the induction principle is already reworked and once theinnerconstructor is changed, the induction principle (recOn') can likely be further improved.