proposition: Theorem getEquivMinSym : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (a : rNat), getEquivMin Ar1 Ar2 a = getEquivMin Ar2 Ar1 a.
proof: Proof. intros Ar1 Ar2 War1 War2 a; unfold getEquivMin in |- *; generalize (getEquivProp3 Ar1 War1 a); generalize (getEquivProp3 Ar2 War2 a); case (getEquiv Ar1 a); case (getEquiv Ar2 a); simpl in |- *. intros L1 b1 L2 b2 OL1 OL2; case b1; case b2; auto with stalmarck; try rewrite (getMinIdSym L1 L2); auto with stalmarck; generalize (getMinInvSym L1 L2); auto with stalmarck; case (getMinInv L1 L2); auto with stalmarck; case (getMinInv L2 L1); auto with stalmarck; intros x1 x2 Hx1 || intros x1 Hx1; auto with stalmarck; generalize (Hx1 OL1 OL2); intros Inv0; inversion Inv0; auto with stalmarck. Qed.