proposition: Lemma SubExp_ScR {Γ Γ' Γ'' τ} (σ : Sub Γ' Γ'') (δ : Ren Γ Γ') (e : Exp Γ'' τ) : SubExp (ScR σ δ) e = RenExp δ (SubExp σ e).
proof: Proof. generalize dependent Γ'. generalize dependent Γ. induction e; simpl; intros; auto; rewrite ?IHe, ?IHe1, ?IHe2, ?IHe3; auto; f_equal. - now rewrite SubVar_ScR. - rewrite <- IHe. unfold Keepₛ. simp ScR. simpl. repeat f_equal. unfold Dropₛ. rewrite !ScR_ScR. unfold skip1; simp RcR. rewrite RcR_idRen_left. now rewrite RcR_idRen_right. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)