Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 23:02:40 -0800 (Mon, 20 Feb 2006)
Revision: 8756
Log message:

      Proved the Itt_hoas_proof_ind.provable_elim1. I've used pairwise functionality
      here to simplify the proof slightly, but this is not necessary as list{BTerm}
      is a sqsimple type.