proposition: Lemma ψP {a: bool} {n: nat} {X: config} : ψ a n (embed X) = match X with | (A, B, x) => ζ (n - length B) (A++[a], B, x) end.
proof: Proof. by rewrite /ψ embedP. 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