Try ltree_finite_BT_bnf

examples/lambda/barendregt/lameta_completeScript.sml

@@ -1333,14 +1333,6 @@ Proof
  >> simp []
 QED
 
-(* NOTE: useless, to be removed *)
-Theorem is_faithful_swap :
-    !p X M N pi r. is_faithful p X [M; N] pi r <=> is_faithful p X [N; M] pi r
-Proof
-    rw [is_faithful_def]
- >> METIS_TAC []
-QED
-
 (*---------------------------------------------------------------------------*
  * Distinct beta-eta-NFs are not everywhere (subtree) equivalent
  *---------------------------------------------------------------------------*)
@@ -1370,6 +1362,19 @@ Theorem BT_to_term_def =
         BT_to_term |> SIMP_RULE std_ss [FUN_EQ_THM, rose_to_term_def, o_DEF]
                    |> Q.SPEC ‘A’ |> GEN_ALL
 
+(* (Test theorem) Boehm tree of a bnf is finite
+
+   NOTE: bnf is already in hnf in all subterms, and is finite, thus the tree
+   is also finite. I think this can be proved by induction on term structure,
+   by nc_INDUCTION2.
+ *)
+Theorem ltree_finite_BT_bnf :
+    !X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ bnf M ==>
+            ltree_finite (BT' X M r)
+Proof
+    cheat
+QED
+
 (* Exercise 10.6.9 [1, p.272] *)
 Theorem distinct_benf_imp_not_subtree_equiv :
     !X M N r. FINITE X /\ X SUBSET FV M UNION FV N /\