Subject: Ssreflect Users Discussion List
List archive
- From: Enrico Tassi <>
- To:
- Subject: Re: Disjoint Cosets (was: big_trivIset)
- Date: Tue, 21 Jun 2011 12:46:29 +0200
On Tue, Jun 21, 2011 at 06:28:53AM -0400, wrote:
> apply: contraR.
> by case/pred0Pn => f /andP [/coset_mem <- /coset_mem <-].
Untested, but the following should work to:
by apply: contraR => /pred0Pn[f /andP[/coset_mem <- /coset_mem <-]].
Or abusing a bit [ ] as I did many times (oops):
by apply: contraR => /pred0Pn[f] /andP[/coset_mem <- /coset_mem <-].
Cheers
--
Enrico Tassi
- big_trivIset, roconnor, 06/20/2011
- Disjoint Cosets (was: big_trivIset), roconnor, 06/20/2011
- Re: Disjoint Cosets (was: big_trivIset), roconnor, 06/21/2011
- Re: Disjoint Cosets (was: big_trivIset), Enrico Tassi, 06/21/2011
- Re: Disjoint Cosets (was: big_trivIset), roconnor, 06/21/2011
- Disjoint Cosets (was: big_trivIset), roconnor, 06/20/2011
Archive powered by MHonArc 2.6.18.