fact: Fixpoint SemTy (τ : Ty) : Type := match τ with | TyUnit => unit | TyPair t1 t2 => SemTy t1 * SemTy t2 | TyArrow dom cod => SemTy dom → SemTy cod end.
imports: Category.Lib Category.Lib.IList Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Equations(Equations)