proposition: Theorem getEquivProp2 : forall (Ar : rArray vM) (War : wellFormedArray Ar) (a : rNat) (c : rZ), snd (getEquiv Ar a) = false -> (In c (fst (getEquiv Ar a)) <-> evalZ Ar c = evalZ Ar (rZPlus a)).
proof: Proof. intros Ar War a c; generalize (getEquivProp Ar War a); case (getEquiv Ar a); auto with stalmarck. intros x; case x; auto with stalmarck. intros b; case b; simpl in |- *; auto with stalmarck. intros H' H'0; discriminate. intros H'; elim H'; auto with stalmarck. intros r l b; case b; simpl in |- *; auto with stalmarck. intros H' H'0; discriminate. intros H'; elim H'; auto with stalmarck. Qed.