]
|generalize in match n4.
elim n2
- [cases n6;simplify;autobatch
+ [cases n6;simplify;
+ [ exists; [2: autobatch;]
+ | exists; [2:autobatch;]
+ ]
|cases n7;simplify
- [autobatch
+ [exists;[2:autobatch]
|elim (H2 n9).
rewrite > H3.
simplify.
- autobatch
+ exists;[2:autobatch]
]]]]]
qed.
\ No newline at end of file