proposition: Lemma env_app_extend {b c} (Γ : env O b) (Δ : env b c) : env_extend Γ (env_app Γ Δ) (env_scope_le Δ).
proof: Proof. depind Δ; subst; intros; autorewrite with env_app scope_le_app in *; simpl; constructor; auto. Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith