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