Induction justification

[CedricMeu]

Allow test case:

theorem sum-z-rh: forall n exists n + (z) = n.
  d1: n + (z) = n by induction on n:

    case z is
      d2: (z) + (z) = (z)	by rule sum-z
    end case
    
    case s n' is
      d3: n' + (z) = n'	by induction hypothesis on n'
      d4: (s n') + (z) = (s n')	by rule sum-s on d3
    end case

  end induction
end theorem

[CedricMeu]

• Show goal on each case.
• Show derivations present in case.
• Show cases left.