proposition: Theorem getEquivProp3 : forall (Ar : rArray vM) (War : wellFormedArray Ar) (a : rNat), OlistRz (fst (getEquiv Ar a)).
proof: Proof. intros Ar War a; generalize (getEquivProp Ar War a); case (getEquiv Ar a); auto with stalmarck. intros x; case x; auto with stalmarck. intros b; case b; intros H'; elim H'; auto with stalmarck. intros r l b; case b; intros H'; elim H'; auto with stalmarck. Qed.