proposition: Lemma decode_subst_encodes (sigma: fin -> exp ag) N x n: encodes (sigma (F x)) n -> decode_subst sigma N x = n.
proof: Proof. intros H; unfold decode_subst. destruct dec_enc as [[m H1]|H1]. - specialize (H a id); asimpl in H. rewrite H in H1. eapply enc_injective in H1 as []; (eauto 2). - exfalso. eapply H1. exists n. specialize (H a id); asimpl in H. now rewrite H. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)