proposition: Lemma ScS_Keepₛ {Γ Γ' Γ'' τ} (f : Sub Γ' Γ'') (g : Sub Γ Γ') : ScS (Keepₛ (τ:=τ) f) (Keepₛ g) = Keepₛ (ScS f g).
proof: Proof. simpl. unfold Keepₛ, Dropₛ. rewrite ScS_ScR. f_equal. rewrite ScR_ScS. f_equal. now rewrite RcS_skip1. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)