proposition: Lemma scope_le_app_len n m (q : scope_le n m) : scope_le_app scope_le_n q = q.
proof: Proof. depind q; simp scope_le_app; trivial. now rewrite IHq. Qed.
imports: Program Equations.Prop.DepElim Equations.Prop.Equations Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Arith