proposition: Lemma subst_equiv s t sigma: s ≡ t -> sigma • s ≡ sigma • t.
proof: Proof. intros (v & ? & ?) % church_rosser; trivial. transitivity (sigma • v); [| symmetry]. all: eapply equiv_star, subst_steps; eauto. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)