1)
                                
                                 f : Unit -> Unit in { f : Unit -> Unit , x : Unit }
                              T-Var ----------------------------------------------- ---------------------------------------- T-Unit
u : Unit in { u : Unit }         f : Unit -> Unit , x : Unit |- f : Unit -> Unit    f : Unit -> Unit, x : Unit |- unit : Unit
-------------------- T-Var         ---------------------------------------------------------------------------------- T-App
u : Unit |- u : Unit                       f : Unit -> Unit , x : Unit |- f unit : Unit
--------------------------------- T-Abs    ------------------------------------------------------- T-Abs
|- (\u : Unit . u) : Unit -> Unit          f : Unit -> Unit |- (\x : Unit . f unit) : Unit -> Unit
-------------------------------------------------------------------------------------------------- T-Let
|- let f = (\ u : Unit . u) in (\x : Unit . f unit) : Unit -> Unit



2) 1. p : Nat × Bool |- λb : Bool . if b then (iszero p.1) else (p.2) : Bool -> Bool

   2. x : { Nat , Bool , Nat , Unit -> Unit , Unit } |- x.4 : Unit -> Unit

   3. r : { age : Nat, name : String } |- iszero (r.age) : Bool



3) Wenn Γ, x : S |- t : T und Γ |- s : S, dann Γ |- [x → s]t : T


   Fall 1 : T-False

     t = false
     T = Bool
     
     dann [x → s]t = [x → s]false = false
     also Γ |- [x → s]t : Bool

   Fall 2 : T-True

   analog

   Fall 3 : T-IfThenElse

     t = if t0 then t1 else t2
     t0 : Bool
     t1 : T
     t2 : T

   laut IV [x → s]t0 : Bool, [x → s]t1 : T, [x → s]t2 : T,

   dann [x → s]if t0 then t1 else t2 = if [x → s]t0 then [x → s]t1 else [x → s]t2
   also Γ |- [x → s]if t0 then t1 else t2 : T

   Fall 4 : T-Var

   t = y

   Fall 4.1 :
   
      x = y
      T = S

     dann [x → s]t = [x → s]x = s
     also Γ |- [x → s]t : S

   Fall 4.2 :

      x != y

     dann [x → s]t = [x → s]y = y = t
     also Γ |- [x → s]t : T

   Fall 5 : T-App

      t = t1 t2
      t1 : T11 -> T
      t2 : T11

   laut IV gilt [x → s]t1 : T11 -> T und [x → s]t2 : T11

   dann [x → s]t = ([x → s]t1) ([x → s]t2)
   also Γ |- [x → s]t : T

   Fall 6 : T-Abs

     t = (λy.t1)
     T = T1 -> T2
     Γ, x:T1 |- t2 : T2

   Fall 6.1 : x == y

     dann [x → s](λx.t1) = λx.t1 = t
     also Γ |- [x → s]t : T

   Fall 6.2 : x != y

    laut IV Γ |- [x → s]t1 : T2

    dann [x → s](λy.t1) = (λx.[x → s]t1)
    also Γ |- [x → s]t : T

  Qed