proposition: Theorem getEquivListProp2 : forall (Ar : rArray vM) (War : wellFormedArray Ar) (a : rZ), OlistRz (getEquivList Ar a).
proof: Proof. intros Ar War a; unfold getEquivList in |- *; case a; intros a'; generalize (getEquivProp3 Ar War a'); case (getEquiv Ar a'); simpl in |- *; auto with stalmarck; intros l b; case b; auto with stalmarck; intros H'; red in |- *; apply Olistf with (eqA := eqRz); auto with stalmarck; exact rZltEqComp. Qed.