Make nested struktural Induktion possible: define sub equations which must be proved and use in their proofs the outer induction hypothesis.