The Coq mailing list

[Taral <taralx AT gmail.com>]

On Tue, Nov 18, 2008 at 6:38 PM, Matthew Brecknell
<coq-club AT brecknell.org>
 wrote:
> I haven't got as far as proving your goal, but here's a more basic
> result you might find useful as a starting point:
>
> Inductive mytest (var : Type) : Type :=
>  | mk_test : var -> mytest var.
>
> Lemma p0: forall (f: forall (fvar: Type), mytest fvar), False.
> Proof (fun f => match (f Empty_set) with mk_test v => Empty_set_ind (fun
> e => False) v end).

Hm, this is interesting, but really takes advantage of the fact that
mk_test has a var. The result I want is really independent of the
constructor arguments. I think I posed my question poorly, since it is
a distillation of a much more complex case.

Inductive test : Type :=
| A : test
| B : test.

Goal forall (f : forall T, T -> test) t x y, f t x = A -> f t y = A.

(Alternatively, f t x = f t y.)

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown