More flexibel reflection solving

[felixwellen]

This is an attempt to solve #521. So far, it is possible to use one variable from context. Like in
the following example:

testWithOneVariable : (x : fst R) → x + 0r ≡ 0r + x
testWithOneVariable x = solveInPlace R x

The solver can be used during equational reasoning like in the following example:

   testWithTwoVariables :  (x y : fst R) → x + y ≡ y + x
   testWithTwoVariables x y =
     x + y                      ≡⟨solveIn R withVars (x ∷ y ∷ []) ⟩
     y + x ∎

However, it is only possible to use the ring solver, if all other variables are introduced
before the ring-variables. This means the following is NOT possible so far:

   testEquationalReasoning' :  (x : fst R) (p : 0r + x ≡ 1r)  → x + 0r ≡ 1r
   testEquationalReasoning' p x =
     x + 0r              ≡⟨solveIn R withVars (x ∷ []) ⟩
     0r + x              ≡⟨ p ⟩
     1r ∎

[felixwellen]

Ohno... Yes, that is what the function actually does.

[ecavallo]

Everything else looks good, I'll merge once Travis is done.

[felixwellen]

Ok, great - thanks!