Proof any CFG can be converted to GNF I studied algorithm for converting grammars to GNF and was wondering about 
a proof that any CFG can be converted into GNF. I found this paper - ENGELFRIET, Joost. An Elementary Proof of Double Greibach Normal Form, 1992, but I do not understand the proof at all. 

Any CFG can be converted into CNF, so we try to prove that any grammar in CNF can be converted into GNF.

At first, a grammar H (not GNF, but can be easily converted into GNF by substitution and by removing rules containing empty string) is constructed from original CNF denoted G as follows:


  1) for rules Y → a
   $$ A \rightarrow  a[Y,A] $$
  2) for rules C → DQ $$ [D,  A] \rightarrow  Q[C,  A] $$
  3) $$ [A,  A] \rightarrow \epsilon $$


Than there are mentioned two statements about this new grammar. These statements are essential for the proof, because they show that the grammar H is equivalent to G. And I do not know why they are right:


  $$
([Y,A] \rightarrow^*_H w) \iff (A \rightarrow ^*_G Y w)
$$
  and
  $$
(A \rightarrow^*_H w) \iff (A \rightarrow ^*_G w)
$$


There is also written that these statements can be shown by induction. I tried to prove them but it seems to me that to prove one of them, I also need to prove the second. So I am stuck at cycle. 

Could somebody please explain it to me?
The textbook proofs of Greibach NF I have seen, contain endless substitutions. This way to construct GrNF is much crisper. 

The key is to understand what the nonterminal $[Y,A]$ actually represents.
It means a derivation that has a leftward "backbone" which starts from $A$ and ends just before $Y$, as in the picture below.



Now the first production in $H$ can be explained as follows. If I start with $A$ and want to produce GrNF then I must generate a terminal. We choose to generate the leftmost terminal $a$ of the subtree under $A$. So, we produce $a$, but we still must find a derivation $[Y,A]$ of the form in the picture, where $Y$ is the nonterminal that actually produces $a$ using the available production $Y\to a$.