proposition: Lemma SubExp_Push {Γ Γ' τ ty} (x : Exp Γ' ty) (s : Sub Γ' Γ) (e : Exp (ty :: Γ) τ) : SubExp (Push x s) e = SubExp {|| x ||} (SubExp (Keepₛ s) e).
proof: Proof. rewrite <- SubExp_ScS. unfold Keepₛ, Dropₛ; simpl. simp SubVar. rewrite ScS_ScR. rewrite RcS_skip1. now rewrite ScS_idSub_right. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)