fact: Fixpoint idSub {Γ} : Sub Γ Γ := match Γ with | [] => NoSub | τ :: Γ => Push (VAR ZV) (ScR (@idSub Γ) skip1) end.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)