proposition: Lemma subst_pointwise_equiv (s: exp X) sigma tau: (forall x, x ∈ vars s -> sigma x ≡ tau x) -> sigma • s ≡ tau • s.
proof: Proof. induction s in sigma, tau |-*; cbn -[vars]; [eauto|eauto|..]. - intros H; eapply equiv_lam_proper, IHs. intros []; cbn -[vars]. reflexivity. intros ? % vars_varof % varofLambda % varof_vars % H. unfold funcomp. now eapply ren_equiv. - intros H; rewrite IHs1, IHs2; eauto. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)