The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi all,
I have a difficulty in the demonstration of a theorem involving type 
classes because for the following class:

Class P_HumHeart {x1:LeftVentricle}{x2:RightVentricle}
                 {x3:LeftAtrium}{x4:RightAtrium}
                 (W:HumanHeart) : Prop  := {
                          ConHH     : Contractility W;
                          PConHH    : Periodic ConHH;
                          LVPOHH    : @IndPartOf x1 W;
                          RVPOHH    : @IndPartOf x2 W;
                          LAPOHH    : @IndPartOf x3 W;
                          RAPOHH    : @IndPartOf x4 W}.

when I try to decompose an object having the type of the class, Coq 
outputs an error due to the dependency between fields (PConHH=f(ConHH). 
If anyone has an idea how to get hypotheses from the above fields?
Thanks in adavance,
Richard

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard