The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Please help me to replace an admission with an actual proof script in this .v 
file. (It seems particularly difficult to specialize over an object variable 
of type C. This is the part I haven't succeeded myself without your help.)

[[[[
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. generalize Other. admit. Save.
End sect.

Axiom ax: forall obj:C, Q num.

Definition C3 := C2(ax).
]]]]

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