proposition: Theorem getRzMinIn1 : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (a : rZ), In (getRzMin Ar1 Ar2 a) (getEquivList Ar1 a).
proof: Proof. intros Ar1 Ar2 War1 War2 a; case a; intros a'; generalize (getEquivMinIn1 Ar1 Ar2 War1 War2 a'); simpl in |- *; auto with stalmarck. case (getEquiv Ar1 a'); auto with stalmarck. intros l b; case b; intros H'; auto with stalmarck. apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. apply in_map; auto with stalmarck. Qed.