[lambda] Boehm_out_lemma (Proposition 10.3.7 (i) [1, p.248])

[binghe]

This PR continue #1205 and finally finishes the proof of "Böhm out lemma" (Proposition 10.3.7 (i) [1, p.248]):

[Boehm_out_lemma] (boehmTheory)
⊢ ∀p X M.
    FINITE X ∧ subterm X M p ≠ NONE ⇒
    ∃pi ss. Boehm_transform pi ∧ apply pi M == subterm' X M p ISUB ss

Note that the antecedent subterm X M p ≠ NONE in the formal version implies the antecedents of the textbook version, by the following new lemma:

[subterm_imp_ltree_paths]
⊢ ∀p X M. FINITE X ∧ subterm X M p ≠ NONE ⇒ p ∈ ltree_paths (BTe X M)

The extra tpm_rel occurred in previous intermediate results (mentioned in previous PR) is now merged into ISUB by the following new lemma about tpm and ISUB (thus does not show up at all in the above final lemma):

[tpm_ISUB_exists] (termTheory)
⊢ ∀pi M. ∃ss. tpm pi M = M ISUB ss

[1] Barendregt, H.P.: The lambda calculus, its syntax and semantics. College Publications, London (1984).

[mn200]

Thanks!