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; trivial. destruct e; reflexivity. now rewrite IHq. Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith