Re: type theory in coq.

Quoting dvanhorn <[email protected]>:

> dvanhorn wrote:
> > Theorem determinacy :
> >   forall t t' t'', (red1 t t') /\ (red1 t t'') -> t'=t''.
> >   intros.
> 
> Theorem determinacy :
>     forall t t', (red1 t t') -> forall t'', (red1 t t'') -> t'=t''.
> induction 1; intros.
> inversion_clear H.
> reflexivity.
> inversion H0.
> inversion_clear H.
> reflexivity.
> inversion H0.
> generalize H; clear H.
> inversion_clear H0; intro H0.
> inversion H0.
> inversion H0.
> rewrite <- IHred1 with (1:=H).
> reflexivity.
> Qed.
> 
> 


Does that mean you'll be giving yourself a dollar?  Buying yourself coffee?  
Patting yourself on the back?  I mean, c'mon, if you'd have given me two more 
months to get around to it, I would've figured it out.  jeez.

-x