Make possible to pove a set of equations which can only be proven at same time.

Tipp: See how coq proof conjunction works with structural induction

Further Idea: Why not add disjunction or implication?