proposition: Lemma list_equiv_ren delta S T: S ≡₊ T -> renL delta S ≡₊ renL delta T.
proof: Proof. intros; pattern S, T; eapply list_equiv_ind; (eauto 2). intros s t S' T' H1 H2 IH; cbn; now rewrite H1, IH. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)