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