The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Let we have some dependent structure. I want several instance proofs every of 
which requires a DIFFERENT but equivalent condition instead of a condition 
specified in the dependent structure.

How to refactor these several proofs to refer to the different condition 
instead of the condition specified in the definition of dependent structure?

An example to be clear:

[[[[
Parameter A: nat->Prop.
Parameter B: nat->Prop.

Axiom First: B O = True.

Axiom Second: B O <-> A O.

Class C := {
  x: nat;
  a: A x
}.

Instance I: C := { x:=O }.
Proof.
Admitted.
]]]]

Here I want to base the proof of I on the axiom First (that is on the 
condition B instead of the condition A which appears in the definition of the 
structure).

You may imagine that I want to prove it for several instances (in the script 
above we have only one instance I, for an example).

-- 
Victor Porton - http://portonvictor.org