type theory in coq.

I've got a dollar for the person who can solve the theorems below (using coq, 
obviously).  I read the online tutorial, but I'll be damned if I can make a 
simple inductive proof.

David



(****************************************************************************)
(*                              _|_  ._  _  _|_|_  _  _ ._  o._   _ _  _.   *)
(*                               |_\/|_)(/_  |_| |(/_(_)|\/ || | (_(_)(_|   *)
(*                                 / |                   /              |   *)
(*                                                                          *)
(*                                                         David Van Horn   *)
(*                                                    [email protected]   *)
(*                                           Sun Feb 29 22:09:44 EST 2004   *)
(*                                                                          *)
(* Exercises from ``Types and Programming Languages'' using the Coq proof   *)
(* assistant.                                                               *)
(*                                                                          *)
(****************************************************************************)

(* Boolean Expressions                                                      *)
(* ===================                                                      *)

Section Boolean_Expressions.     (* Fig 3.1 in Pierce's TAPL. *)

Inductive term : Set :=
   | true : term
   | false : term
   | If : term -> term -> term -> term.

(* How do I make subtypes? *)
(* Inductive v : Set := true : v | false : v. *)
Definition value (t : term) :=
   t=true\/t=false

(* The single step reduction relation, ->                                   *)

Inductive red1 : term -> term -> Prop :=
   | E_IfTrue  : forall t2 t3 : term, (red1 (If true t2 t3) t2)
   | E_IfFalse : forall t2 t3 : term, (red1 (If false t2 t3) t3)
   | E_If : forall t1 t1': term, (red1 t1 t1') ->
              (forall t2 t3 : term, (red1 (If t1 t2 t3) (If t1' t2 t3))).


(* The multi step evaluation relation, ->*                                  *)
(* reflexive, transitive closure of ->                                      *)

Inductive red : term -> term -> Prop :=
   | red_one_step : forall t t', (red1 t t') -> (red t t')
   | red_refl : forall t, (red t t)
   | red_trans : forall t t' t'', (red t t') -> (red t t'') -> (red t t'').


Theorem determinacy :
   forall t t' t'', (red1 t t') /\ (red1 t t'') -> t'=t''.
   intros.

Definition normal_form (t : term) :=
   forall t', ~(red1 t t').

Theorem value_implies_normal :
   forall t, (value t) -> (normal_form t).

Theorem normal_implies_value :
   forall t, (normal_form t) -> (value t).

Theorem confluence :
   forall t u u', (red t u) /\ (red t u') /\ (normal u) /\ (normal u') -> u=u'.

Theorem termination :
   forall t, (exists t', (red t t')).