The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 10 Apr 2006, Adam Koprowski wrote:

> Variable A: Set.
> Inductive Test: Set :=
> | Elem: A -> Test
> | Pair: Test -> Test -> Test.
>
> Fact discr: forall a b, ~a = Pair a b.
> Proof. ?

I have the following

Fact discr: forall a b, ~a = Pair a b.
Proof.
induction a; intros b H.
discriminate H.
inversion H.
firstorder.
Qed.

Perhaps there is a nicer way.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''