add substitution for proof, we will require closed conditions for proof tactic
realized I need to implement capture avoiding for proof red.
implement the cap-avoid for proof
dealing with parser support for tactics
run into a problem of distinguishing proof var and term var
need to re-engineer the proof parser
now parser support the tactic language
handle two form of discharge.
need to stop now, need to fix a bug on app proof
fix the nasty bug on app proof
implement a transformation from prscr to proof, now ready to test tactic and all that
testing tactic
internal proof substitution is captured intended.
this is awesome, seems like tactic is a good idea
decided to go with weak head reduction for future optimization on the program
some editting
Merge branch 'prog-proof'