open LTO
  pr(INDUCTIONOFLEADSTO(PNAT)) .
-- cehck if the property holds
  red lto16(s,i,n) => lto17(s,i) .
close