Theorem nthext2 | index | src |

theorem nthext2 (l1 l2 n: nat) {i: nat}:
  $ len l1 = n $ >
  $ len l2 = n $ >
  $ i < n -> nth i l1 = nth i l2 $ >
  $ l1 = l2 $;
StepHypRefExpression
1 hyp h1
len l1 = n
2 1 a1i
T. -> len l1 = n
3 hyp h2
len l2 = n
4 3 a1i
T. -> len l2 = n
5 hyp h3
i < n -> nth i l1 = nth i l2
6 5 anwr
T. /\ i < n -> nth i l1 = nth i l2
7 2, 4, 6 nthext2d
T. -> l1 = l2
8 7 trud
l1 = l2

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)