Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] C-zar proof help

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] C-zar proof help


chronological Thread 
  • From: Taral <taralx AT gmail.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] C-zar proof help
  • Date: Tue, 3 Mar 2009 14:53:18 -0800
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; b=JqVKwyLc+cjate2OwH9wVOjStT+e1uR4UiY453fdQ3x1cdBQJcY3oFG/nIf0yNztP8 /LOKHDmU/7uHOQJORW2IVF6VDa/nHec1GiMBGK7u7H2yIn7XNvdxZn9fYlfh72D/10NV tGl5n1vSyp76CPtcOfDpeMrHcmi8A1W8myXI8=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Tue, Mar 3, 2009 at 2:43 PM, Taral 
<taralx AT gmail.com>
 wrote:
> You need to expose (commute (up, uq)) before taking cases on it. Also,
> you cannot extract the hypothesis if you are going to case on a
> subexpression.

Does anyone know why "per cases on A. suppose it is B." doesn't just
introduce "A = B" as a hypothesis?

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



Archive powered by MhonArc 2.6.16.

Top of Page