- apply (exchangeL ? a1 a2 (FAtom a));
- apply (exchangeR ? a3 a4 (FAtom a));
- apply axiom
- | elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2);
+ apply (ExchangeL ? a2 a3 (FAtom a1));
+ apply (ExchangeR ? a4 a5 (FAtom a1));
+ apply Axiom
+ | elim (sizel_0_no_axiom_is_tautology a b H H1 H2);