proposition: Lemma list_equiv_anti_ren delta (S T: list (exp X)): Injective delta -> renL delta S ≡₊ renL delta T -> S ≡₊ T.
proof: Proof. intros In. remember (renL delta S) as S'. remember (renL delta T) as T'. intros H; revert S T HeqS' HeqT'; pattern S', T'. eapply list_equiv_ind; (eauto 2). all: intros. - destruct S, T; try discriminate. reflexivity. - destruct S0, T0; try discriminate. injection HeqS' as ??; injection HeqT' as ??; subst. eapply equiv_lstep_cons_proper; (eauto 2). eapply equiv_anti_ren; (eauto 2). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)