proposition: Lemma lookup_app : forall {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. intros n Γ m Δ; induction Δ; intros x; simpl... destruct e... rewrite IHΔ... Qed.
imports: Equations.Equations Equations.DepElimDec Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Program Arith