proposition: Lemma SubExp_ScS {Γ Γ' Γ'' τ} (σ : Sub Γ' Γ'') (δ : Sub Γ Γ') (e : Exp Γ'' τ) : SubExp (ScS σ δ) e = SubExp δ (SubExp σ e).
proof: Proof. generalize dependent Γ'. generalize dependent Γ. induction e; simpl; intros; auto; rewrite ?IHe, ?IHe1, ?IHe2, ?IHe3; auto; f_equal. - now rewrite SubVar_ScS. - rewrite <- IHe; clear. f_equal. unfold Keepₛ. unfold Dropₛ. simpl. simp SubVar. f_equal. rewrite ScR_ScS. remember (ScR δ skip1) as g; clear. unfold skip1. generalize dependent g. generalize dependent Γ0. induction σ; simpl; simp ScR; simpl; intros; auto. f_equal; auto. rewrite <- SubExp_RcS. simp RcS. now rewrite RcS_idRen. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)