some progress towards substitution proofs
Merge pull request #1 from Zeldy/master

some progress towards substitution proofs