Exception in thread "main" java.util.NoSuchElementException: key not found: s_0
	at scala.collection.immutable.Map$Map2.apply(Map.scala:129)
	at gapt.proofs.reduction.ErasureReductionHelper.i$1(manySorted.scala:125)
        <snip>

  implicit var ctx = Context.default
  ctx += Context.InductiveType( "nat", hoc"0: nat", hoc"s: nat>nat" )
  ctx += Notation.Infix( "<", Precedence.infixRel )
  ctx += hoc"'<': nat>nat>o"

  val lt = hof"!x (s x) < (s(s x))"

  ( Vampire.extendToManySortedViaErasure ) getExpansionProof ( lt +: Sequent() :+ lt )