proposition: Theorem getEquivListProp4 : forall (Ar : rArray vM) (War : wellFormedArray Ar) (S : State), rArrayState Ar S -> forall a b : rZ, eqStateRz S a b <-> getEquivList Ar a = getEquivList Ar b.
proof: Proof. intros Ar War S Sar a b; red in |- *; split; intros H'1; auto with stalmarck. cut (EqL _ (eq (A:=rZ)) (getEquivList Ar a) (getEquivList Ar b)). intros H'; elim H'; simpl in |- *; auto with stalmarck. intros a0 b0 L1 L2 H'0 H'2 H'3; rewrite H'0; rewrite H'3; auto with stalmarck. apply EqLOlist with (ltA := rZlt); try (red in |- *; auto with stalmarck; fail); auto with stalmarck. intros a0 b0 H'; red in |- *; intros H'0; absurd (rZlt a0 b0); auto with stalmarck; rewrite H'0; auto with stalmarck. intros a0 b0 c d H' H'0 H'2; rewrite <- H'0; rewrite <- H'2; auto with stalmarck. apply getEquivListProp2; auto with stalmarck. apply getEquivListProp2; auto with stalmarck. apply InclEqDef; auto with stalmarck. intros a0 H'; apply inImpInEq; auto with stalmarck. red in |- *; auto with stalmarck. case (getEquivListProp1 Ar War b a0). intros H'0 H'2; apply H'2; auto with stalmarck. apply trans_equal with (evalZ Ar a). case (getEquivListProp1 Ar War a a0). intros H'3 H'4; apply H'3. elim H'; simpl in |- *; auto with stalmarck. apply rArrayStateDef1 with (S := S); auto with stalmarck. apply InclEqDef; auto with stalmarck. intros a0 H'; apply inImpInEq; auto with stalmarck. red in |- *; auto with stalmarck. case (getEquivListProp1 Ar War a a0). intros H'0 H'2; apply H'2. apply trans_equal with (evalZ Ar b). case (getEquivListProp1 Ar War b a0). intros H'3 H'4; apply H'3. elim H'; simpl in |- *; auto with stalmarck. apply rArrayStateDef1 with (S := S); auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. case (getEquivListProp1 Ar War b a); auto with stalmarck. intros H' H'0; apply H'. rewrite <- H'1. apply getEquivListProp3; auto with stalmarck. Qed.