Add last declarative tactics, modify rewriting tactics

Add last declarative tactics, modify rewriting tactics

Add types for induction and case analysis to grafiteAst. Add new types
for obtain and conclude

Add pp code for induction, case, obtain, conclude

Add calls in grafiteEngine for induction, case, obtain, conclude

Add parsing rules for induction, case, obtain, conclude

Rename a function for code clarity

Add function to swap two goals on the stack (useful for obtain)

Add a conclude function that checks that the given term is the lhs of
the current goal

Add a obtain function that starts an equality chain beginning with the
given term in a new goal

Modify rewriting step to only handle single equality chains steps

Add implementation for induction and case.

Add signatures for induction, case, conclude, obtain

Add keywords to matita.lang for induction, case, conclude, obtain