Skip to Content.
Sympa Menu

ssreflect - [ssreflect] Question of style

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Question of style


Chronological Thread 
  • From: bertot <>
  • To: ssreflect <>
  • Subject: [ssreflect] Question of style
  • Date: Tue, 05 Nov 2013 15:11:53 +0100

Hello,

I am using poly.v and I need to reduce

- 'X \Po p

into -p

It seems that there is a theorem missing, with name
comp_poly_opp and statement

-p \Po q = -(p \Po q)

or something semantically equivalent. Do you agree?

Yves



Archive powered by MHonArc 2.6.18.

Top of Page