proposition: Lemma SubSem_inil (s : Sub nil nil) : SubSem s () = ().
proof: Proof. now dependent elimination s. Qed.
imports: Category.Lib Category.Lib.IList Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Equations(Equations)