proposition: Lemma SubExp_RcS {Γ Γ' Γ'' τ} (σ : Ren Γ' Γ'') (δ : Sub Γ Γ') (e : Exp Γ'' τ) : SubExp (RcS σ δ) e = SubExp δ (RenExp σ e).
proof: Proof. generalize dependent Γ'. generalize dependent Γ. induction e; simpl; intros; auto; rewrite ?IHe, ?IHe1, ?IHe2, ?IHe3; auto; f_equal. - now rewrite SubVar_RcS. - specialize (IHe _ _ (Keep σ) (Keepₛ δ)). rewrite <- IHe. unfold Keepₛ. simp RcS. repeat f_equal. unfold Dropₛ. now apply ScR_RcS. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)