proposition: Lemma descendP {s t: term} {B: list symbol} : descend s B = Some t -> length B <= term_depth_bound s.
proof: Proof. elim: B s t; first by (move=> /= *; lia). move=> b B IH [ /= | > /IH]; [done | case: b => /=; by lia]. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.StackMachines(SSM) Undecidability.StackMachines.Util(CSSM_facts) Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool