proposition: Lemma ascend_arr {ψ0 ψ1: valuation} {s t: term} {A: stack} : ascend ψ0 ψ1 (arr s t) A = arr (ascend ψ0 ψ1 s A) (ascend ψ0 ψ1 t A).
proof: Proof. elim: A s t; first done. move=> a A IH s t /=. by rewrite IH. 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