proposition: Lemma subst_varof x sigma y (s: exp X): varof y s -> varof x (sigma y) -> varof x (sigma • s).
proof: Proof. induction 1 in sigma, x |-*; cbn; eauto. intros H'; econstructor; eapply IHvarof; cbn; unfold funcomp. now eapply ren_varof. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)