Solution of a Problem of Barendregt on Sensible lambda-Theories
  <i>H</i> is the theory extending &#946;-conversion by identifying all closed unsolvables. <i>H</i>&#969; is the closure of this theory under the &#969;-rule (and &#946;-conversion). A long-standing conjecture of H. Barendregt states that the provable equations of <i>H</i>&#969; form &#928;<sub>1</sub><sup>1</sup>-complete set. Here we prove that conjecture. 
Benedetto Intrigila and Richard Statman