proposition: Lemma sa_weakening : forall {b} (Γ : env O b) p q (A : sa Γ p q) {c P} (Δ : env O c) (B : env_extend Γ Δ P), sa Δ (lift_type_by P p) (lift_type_by P q).
proof: Proof. intros b Γ p q A; induction A; intros c P Δ B; autorewrite with lift_type_by in *; try (auto; constructor; auto; fail). - depelim c; [depelim B|]. constructor; rewrite <- (env_extend_lookup _ _ _ B); auto. - constructor; auto. eapply IHA2. constructor. auto. Qed.
imports: Equations.Equations Equations.DepElimDec Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Program Arith