proposition: Theorem getEquivInter : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S S1 S2 : State), rArrayState Ar1 S1 -> rArrayState Ar2 S2 -> (forall a : rNat, eqStateRz S (rZPlus a) (getEquivMin Ar1 Ar2 a)) -> inclState (interState S1 S2) S.
proof: Proof. intros Ar1 Ar2 War1 War2 S S1 S2 H' H'0 H'1. red in |- *; auto with stalmarck. intros i j H'2. cut (eqStateRz S1 i j); [ intros Em1 | apply eqStateIncl with (2 := H'2) ]; auto with stalmarck. cut (eqStateRz S2 i j); [ intros Em2 | apply eqStateIncl with (2 := H'2) ]; auto with stalmarck. case (rZDec i j); intros Eqij; auto with stalmarck. rewrite Eqij; auto with stalmarck. apply eqStateRzTrans with (b := getRzMin Ar1 Ar2 i). apply forallgetEquivgetRzMin; auto with stalmarck. rewrite (getRzMinUnique Ar1 Ar2 War1 War2 S1 S2 H' H'0 i j); auto with stalmarck. apply eqStateRzSym; auto with stalmarck. apply forallgetEquivgetRzMin; auto with stalmarck. Qed.