proposition: Lemma backward_vars x: sigma • fst (varEQ x) ≡ sigma • snd (varEQ x) -> exists n, encodes (sigma (F x)) n.
proof: Proof. Proof using N. cbn; simplify. unfold funcomp; change shift with (add 1); rewrite ren_plus_combine; unfold var_zero; cbn. intros H; eapply normal_forms_encodes in H; (eauto 2). Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)