(**************************************************************************)
include "basic_2/syntax/tdeq.ma".
-include "basic_2/relocation/lifts.ma".
+include "basic_2/relocation/lifts_lifts.ma".
(* GENERIC RELOCATION FOR TERMS *********************************************)
]
qed-.
+lemma tdeq_lifts_bi: ∀h,o. liftable2_bi (tdeq h o).
+/3 width=6 by tdeq_lifts, liftable2_sn_bi/ qed-.
+
(* Inversion lemmas with degree-based equivalence for terms *****************)
lemma tdeq_inv_lifts: ∀h,o. deliftable2_sn (tdeq h o).
/3 width=5 by lifts_flat, tdeq_pair, ex2_intro/
]
qed-.
+
+lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o).
+/3 width=6 by tdeq_inv_lifts, deliftable2_sn_bi/ qed-.