simplified top-level equivalence theorem, got rid of lemmas ll44 and ll45