Improved subtree_equiv_lemma without subtree_equiv'

[binghe]

Hi,

This PR improves the previous #1367. With an improved construction of Böhm transform (beyond textbook), I have removed the needs of subtree_equiv' and proved a better version of subtree_equiv_lemma (NOTE: In previous PR the theorem name was wrongly written in the code as subterm_equiv_lemma, this typo is fixed here.):

[subtree_equiv_lemma]
⊢ ∀X Ms p r.
    FINITE X ∧ p ≠ [] ∧ 0 < r ∧ Ms ≠ [] ∧
    BIGUNION (IMAGE FV (set Ms)) ⊆ X ∪ RANK r ∧
    EVERY (λM. subterm X M p r ≠ NONE) Ms ⇒
    ∃pi.
      Boehm_transform pi ∧ EVERY is_ready' (MAP (apply pi) Ms) ∧
      (∀M. MEM M Ms ⇒ p ∈ ltree_paths (BT' X (apply pi M) r)) ∧
      ∀M N q.
        MEM M Ms ∧ MEM N Ms ∧ q ≼ p ⇒
        (subtree_equiv X M N q r ⇔
         subtree_equiv X (apply pi M) (apply pi N) q r)

The previous added definitions subtree_equiv' and ltree_equiv', etc. are now useless and removed.

NOTE: For the next applications of this lemma, the antecedent EVERY (λM. subterm X M p r ≠ NONE) Ms may still need to be weaken to p ∈ ltree_paths (BT' X M r)) or even completely eliminated, and the involved is_ready' (a variant of is_ready) can then be recovered to the original is_ready. These changes will bring a few more trivial cases and further increases the proof size (now boehmScript.sml has more than 10K lines.)

--Chun

[mn200]

Seems promising!