Add a revert transformation
Make a general revert transformation.
"revert x" should transform a context:
Delta, x: t, Delta' |- G
Delta, x : t |- Delta' "->" G
with "->" meaning -> for hypotheses and forall quantification for symbols.
Eventually use this revert for other transformations like induction, induction_pr etc