corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant

quick_and_dirty := true;
no_document use_thys ["LaTeXsugar"];
use_thys ["Paper"];