proposition: Lemma sa_weakening_app : forall {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: Equations.Equations Equations.DepElimDec Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Program Arith