The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Dear Adam,

Adam Chlipala wrote:
> > Your theorem above tie things down quite nicely - many thanks for 
> > that. But I was also wondering (for curiosity sake more than anything 
> > else) whether <-> could be replaced by ->, if the implicand 
> > constrained Y to be the smallest possible list. If that were possible, 
> > (X p') wouldn't then be a witness.
>
> Do you have some convention in mind for doing such constraining with an 
> implication?  I've never seen such a feature in logic or math, on paper 
> or on a computer.  You could certainly do it with an extra conjunction 
> and universally-quantified fact, though.

I hope I've used the right terminology. I suggested constraining the implicand, 
not the implication. As far as I'm aware, the implicand is the conclusion of the 
implication.

Regards,
Jeff.