proposition: Lemma env_extend_lookup : forall {b c} (Γ : env O b) (Δ : env O c) P, env_extend Γ Δ P -> forall x, lift_type_by P (lookup Γ x) = lookup Δ (lift_var_by P x).
proof: Proof. Proof with autorewrite with lift_type_by lift_var_by map_var lookup scope_le_app; auto. intros b c Γ Δ P A; depind A; intros x; depelim x... all:rewrite <- IHA... Qed.
imports: Equations.Equations Equations.DepElimDec Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Program Arith