proposition: Lemma sa_toname {n m} Γ (Δ : env (S n) m) x : x <> lift_var_by (env_scope_le Δ) FO -> forall p q, lookup (env_app (cons p Γ) Δ) x = lookup (env_app (cons q Γ) Δ) x.
proof: Proof. depind Δ; subst; intros A p q; depelim x; simpl in *; autorewrite with env_app lookup lift_var_by in *; auto. - exfalso; auto. - specialize (IHΔ Γ x). forward IHΔ by intro; subst; auto. now rewrite (IHΔ p q). Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith