proposition: Lemma lookup_app {n} (Γ : env O (S n)) {m} (Δ : env (S n) (S m)) x : lookup (env_app Γ Δ) (lift_var_by (env_scope_le Δ) x) = lift_type_by (env_scope_le Δ) (lookup Γ x).
proof: Proof. Proof with autorewrite with lookup scope_le_app env_app lift_var_by lift_type_by; auto. induction Δ; subst; simpl... rewrite IHΔ... Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith