Re: type theory in coq.
dvanhorn <[email protected]>
| Newsgroups | gmane.org.ballistichelmet.lambda |
|---|---|
| Message-ID | <[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.