Theorem listind | index | src |

theorem listind {x a l: nat} (n: nat) (px: wff x) (p0 pn: wff) (pl: wff l)
  (ps: wff a l):
  $ x = n -> (px <-> pn) $ >
  $ x = 0 -> (px <-> p0) $ >
  $ x = l -> (px <-> pl) $ >
  $ x = a : l -> (px <-> ps) $ >
  $ p0 $ >
  $ pl -> ps $ >
  $ pn $;
StepHypRefExpression
1 hyp hn
x = n -> (px <-> pn)
2 hyp h0
x = 0 -> (px <-> p0)
3 hyp hl
x = l -> (px <-> pl)
4 hyp hs
x = a : l -> (px <-> ps)
5 hyp h1
p0
6 5 a1i
T. -> p0
7 hyp h2
pl -> ps
8 7 anwr
T. /\ pl -> ps
9 1, 2, 3, 4, 6, 8 listindd
T. -> pn
10 9 trud
pn

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)