proposition: Lemma env_scope_le : forall {n m}, env n m -> scope_le n m.
proof: Proof. intros n m Γ; depind Γ; constructor; auto. Defined.
imports: Program Equations.Prop.DepElim Equations.Prop.Equations Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Arith