The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

I guess the problem is that the expression "C2" of type "C" cannot be
applied to the term "ax2" : "forall obj : C, Q num".

Cheers

Alexandre

On Mon, Nov 14, 2011 at 9:41 AM, Victor Porton 
<porton AT narod.ru>
 wrote:
> Hypothesis P: nat->Prop.
> Hypothesis Q: nat->Prop.
>
> Axiom Eq: forall x:nat, P(x)<->Q(x).
>
> Class C := {
> šnum: nat;
> šcond: P num
> }.
>
> Section sect.
> šHypothesis Other: forall obj:C, Q num.
>
> šInstance C2: C := { num:=0 }.
> šProof. Admitted.
> End sect.
>
> Axiom ax2: forall obj:C, Q num.
>
> Definition C3 := C2(ax2).