proposition: Lemma nf_equiv (X: config) : equiv X (nf X).
proof: Proof. Proof using confluent_M. rewrite /nf. move: (embed X) => i. elim: i X. { move=> X /=. by apply: equiv_refl. } move=> i IH X /=. case: (equiv_dec (unembed i) X). { move=> /equiv_sym H /=. apply: (equiv_trans confluent_M H). by apply: IH. } move=> /= _. by apply: 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