proposition: Lemma nf_equiv_eq_ind (X Y: config) (j: nat) : equiv X Y -> embed X < j -> nf_aux j Y = nf_aux (embed X) X.
proof: Proof. Proof using confluent_M. elim: j X Y; first by lia. move=> i IH X Y HXY HXi /=. case: (equiv_dec (unembed i) Y)=> /=. { move=> /equiv_sym HYi. have [/[dup] [/(f_equal unembed) + ->] | ?]: (embed X = i \/ embed X < i) by lia. - rewrite embedP. by move=> ->. - apply: IH; [ apply: equiv_trans; by eassumption | done]. } move=> HiY. have [/(f_equal unembed) | ?]: (embed X = i \/ embed X < i) by lia. - rewrite embedP. move=> ?. by subst X. - 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