theory Scratch
  imports Main
begin

lemma
  assumes "True"
    and "True"
  shows "True"
  ..

end