Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. R : Alph List Alph List

  3. n :

  4. x:Alph List. R x x

  5. x,y:Alph List. R x y R y x

  6. x,y,z:Alph List. R x y R y z R x z

  7. x,y,z:Alph List. R x y R (z @ x) (z @ y)

  8. w : n Alph List

  9. l:Alph List. i:n. R l (w i)

  10. a : Alph List

  11. b : Alph List

  12. c : Alph List

  13. ||a|| n * n

Conclusion:

a':Alph List. ||a'|| < ||a|| R (a @ b) (a' @ b) R (a @ c) (a' @ c)

Applied Tactic: InstLemma `ax_choice` [Alph List;n;l i.R l (w i)] THENA Auto THEN D 14
Generated subgoals:

1. a':Alph List. ||a'|| < ||a|| R (a @ b) (a' @ b) R (a @ c) (a' @ c)