proposition: Lemma sa_weakening_app {b} (Γ : env O b) p q (A : sa Γ p q) {c} (Δ : env b c) : sa (env_app Γ Δ) (lift_type_by (env_scope_le Δ) p) (lift_type_by (env_scope_le Δ) q).
proof: Proof. intros; eapply sa_weakening. exact A. auto using env_app_extend. Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith