- [ lapply add_gen_O_2 to H using H0. clear H.
- rewrite > H0. clear H0. clear p1
- | lapply add_gen_S_2 to H1 using H0. clear H1.
- decompose H0.
- rewrite > H3. rewrite > H3 in H2. clear H3. clear r1.
- lapply add_gen_S_2 to H2 using H0. clear H2.
- decompose H0.
- rewrite > H2. clear H2. clear r2.
- lapply H to H4, H3 using H0. clear H. clear H4. clear H3.
- decompose H0.
- ]; apply ex_intro; [| auto || auto ].
+ [ lapply add_gen_O_2 to H as H0. clear H.
+ rewrite > H0. clear H0 p1
+ | lapply add_gen_S_2 to H1 as H0. clear H1.
+ decompose.
+ rewrite > H3. rewrite > H3 in H2. clear H3 r1.
+ lapply add_gen_S_2 to H2 as H0. clear H2.
+ decompose.
+ rewrite > H2. clear H2 r2.
+ lapply H to H4, H3 as H0. clear H H4 H3.
+ decompose.
+ ]; apply ex_intro; [| auto || auto ]. (**)