proposition: Lemma forward_vars x n: encodes (sigma (F x)) n -> sigma • fst (varEQ x) ≡ sigma • snd (varEQ x).
proof: Proof. intros H. unfold varEQ; cbn; unfold funcomp. change shift with (add 1); rewrite ren_plus_combine, !H; cbn; unfold var_zero. change (g a (var 1)) with (enc 1 (var 1)); now simplify. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)