+ [ apply (H x2 x1 x3 ? ?);
+ [apply (sym x1 x2 ?).
+ apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
+ | apply (H x1 x3 x ? ?);
+ [apply (H x1 x2 x3 ? ?);
+ [apply (H1).
+ |apply (H3).
+ ]
+ |apply (sym x x3 ?).
+ apply (H2).
+ ]
+ ]