proposition: Theorem wfDisjoint : forall (r s : rNat) (Lr Ls : list rZ), s <> r -> get Ar r = class Lr -> get Ar s = class Ls -> DisjointRz Lr Ls.
proof: Proof. intros r s Lr Ls H' H'0 H'1; red in |- *; apply DisjointDef. intros a H'2; red in |- *; intros H'3; case H'. case (InEqInv _ _ H'2); intros In1; generalize (wfPcc1 _ _ _ H'0 In1); intros get1; case (InEqInv _ _ H'3); intros In2; generalize (wfPcc1 _ _ _ H'1 In2); intros get2. apply refSameEq with (a := a) (b := a); rewrite <- get1; rewrite <- get2; auto with stalmarck. apply refSameEq with (a := rZComp a) (b := a); rewrite <- get1; rewrite <- get2; auto with stalmarck. case a; simpl in |- *; auto with stalmarck. apply refSameEq with (a := a) (b := rZComp a); rewrite <- get1; rewrite <- get2; auto with stalmarck. case a; simpl in |- *; auto with stalmarck. apply refSameEq with (a := rZComp a) (b := rZComp a); rewrite <- get1; rewrite <- get2; auto with stalmarck. Qed.