Theorem rlistind ≪ | index | src

theorem rlistind {x l a: nat} (n: nat) (px: wff x) (p0 pn: wff) (pl: wff l)
  (ps: wff l a):
  $ x = n -> (px <-> pn) $ >
  $ x = 0 -> (px <-> p0) $ >
  $ x = l -> (px <-> pl) $ >
  $ x = l |> a -> (px <-> ps) $ >
  $ p0 $ >
  $ pl -> ps $ >
  $ pn $;

x = n -> (px <-> pn)

x = 0 -> (px <-> p0)

x = l -> (px <-> pl)

x = l |> a -> (px <-> ps)

p0

T. -> p0

pl -> ps

T. /\ pl -> ps

T. -> pn

pn

Axiom use