Messages of different lengths and one-time computationally-secret

I'm preparing myself to exam, but I have a lot of troubles with rigorous proofs.

Let $\Pi=(Gen,Enc,Dec)$ be an efficient secret-key encryption scheme that is not fixed-length. That is, for any $n$ and any $k \leftarrow Gen(1^n)$ the encryption algorithm $Enc_k(\cdot)$ can encrypt arbitrary length messages $m \in \lbrace 0, 1 \rbrace^*$.

Prove that $\Pi$ cannot satisfy definition of being one-time computationally-secret when the adversary $\mathcal{A}$ in $PrivK^{eav}_{\mathcal{A}}$ may output messages $m_0$ and $m_1$, that are NOT of the same length.

I just can (I think so) start this proof - if $Enc_k(\cdot)$ is some PPT algorithm, then there exists a polynomial $p(x) \in \mathbb{Z}[x]$ such that

$\forall n,k \leftarrow Gen(1^n), m \in \lbrace 0, 1 \rbrace^*: ||Enc_k(m)||<p(||k||+||m||)$.

Unfortunately I have no idea how to do the rest of the proof - by contradiction, or not? If you could help me with the rigorous proof, I'd be really grateful for your time.

P.S. Reminder (one-time computationally-secret).

An (efficient secret-key) encryption scheme $(Gen,Enc,Dec)$ is one-time computationally-secret if for any PPT adversary $\mathcal{A}$ it holds that $Pr[PrivK^{eav}_{\mathcal{A}}(n)=1]-\frac{1}{2}$ is negligible function, where $PrivK^{eav}_{\mathcal{A}}(n)$ denotes the output of the following experiment:

(a) The adversary $\mathcal{A}$ on input $1^n$ outputs a pair of messages $m_0,m_1$.

(b) Let $k \leftarrow Gen(1^n)$ and let $b \in \lbrace 0,1 \rbrace$ be chosen uniformly at random. Then a ciphertext $c \leftarrow Enc_k(m_b)$ is computed and given to $\mathcal{A}$.

(c) $\mathcal{A}$ on input $c$ outputs a bit $b'$.

(d) The output of the experiment is $1$ if $b'=b$ and $0$ otherwise.

-
Hint: The adversary needs to construct two messages such that their ciphertexts are of different length. Use the efficiency condition to show that this is always possible. – Paŭlo Ebermann Oct 28 '12 at 20:11
If this is not enough, have a look at our recent questions Why is a non fixed-length encryption scheme worse than a fixed-length one? and How to construct a variable length IND-CPA cipher from a fixed length one? (including the discussion in the comments). – Paŭlo Ebermann Oct 28 '12 at 20:24
What is efficiency condition? Could you tell me a little bit more how should the formal proof be looking like? I think I know what is the idea, but I have big problem with writing it down rigorously. Thank you. – BiggBen1989 Oct 30 '12 at 0:01
Look up the meaning of the word "efficient" in your definition. (It means something like "a short input will only take a short time", and as such it can also only have a short output. But look it up in your literature.) – Paŭlo Ebermann Nov 1 '12 at 13:07

To turn it into a formal proof, write down an adversary $A$ that breaks the security of $\Pi$. You may want to first work out the attack at a conceptual level to make sure you are clear on how to attack $\Pi$; then review the definition of what it means for an adversary to break $\Pi$; then turn your conceptual attack into a fully specified algorithm $A$, and check that it does indeed break $\Pi$.