proposition: Lemma nf_equiv_eq (X Y: config) : equiv X Y -> nf X = nf Y.
proof: Proof. Proof using confluent_M. have: (embed X = embed Y \/ embed X < embed Y \/ embed Y < embed X) by lia. case; [|case]. - move /(f_equal unembed). rewrite ? embedP. by move=> ->. - move=> + H. move /nf_equiv_eq_ind. by move /(_ _ H). - move=> + /equiv_sym H. move /nf_equiv_eq_ind. by move /(_ _ H). 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