proposition: Theorem getEquivListProp1 : forall (Ar : rArray vM) (War : wellFormedArray Ar) (a c : rZ), In c (getEquivList Ar a) <-> evalZ Ar c = evalZ Ar a.
proof: Proof. intros Ar War a; unfold getEquivList in |- *; case a; intros a'; generalize (getEquivProp1 Ar War a'); generalize (getEquivProp2 Ar War a'); case (getEquiv Ar a'); simpl in |- *; auto with stalmarck; intros l b; case b; auto with stalmarck. intros H' H'0 c. lapply (H'0 c); [ intros H'1; red in H'1 | idtac ]; auto with stalmarck. Elimc H'1; intros H'1 H'2. red in |- *; split; intros H'3; auto with stalmarck. apply H'1; auto with stalmarck. apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. rewrite (rZCompInvol c); apply in_map; auto with stalmarck. intros H' H'0 c. lapply (H'0 (rZComp c)); [ rewrite <- rZCompInvol; intros H'1; red in H'1 | idtac ]; auto with stalmarck. Elimc H'1; intros H'1 H'2. red in |- *; split; intros H'3; auto with stalmarck. rewrite <- H'1; auto with stalmarck. rewrite (evalZComp Ar c); auto with stalmarck. apply H'2; auto with stalmarck. rewrite (evalZComp Ar c); auto with stalmarck. rewrite H'3; auto with stalmarck. intros H' H'0 c. lapply (H' (rZComp c)); [ intros H'1; red in H'1 | idtac ]; auto with stalmarck. Elimc H'1; intros H'1 H'2. red in |- *; split; intros H'3; auto with stalmarck. rewrite <- H'1; auto with stalmarck. rewrite (evalZComp Ar c); auto with stalmarck. apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. rewrite (rZCompInvol c); apply in_map; auto with stalmarck. apply H'2; auto with stalmarck. rewrite (evalZComp Ar c); auto with stalmarck. rewrite H'3; auto with stalmarck. Qed.