Nuprl Lemma : list_ind_cons_lemma
∀A,x,b,a:Top. (rec-case([a / b]) of [] => x | h::t => r.A[h;t;r] ~ A[a;b;rec-case(b) of [] => x | h::t => r.A[h;t;r]])
Proof
Error : references
Latex:
\mforall{}A,x,b,a:Top.
(rec-case([a / b]) of
[] => x
h::t =>
r.A[h;t;r] \msim{} A[a;b;rec-case(b) of
[] => x
h::t =>
r.A[h;t;r]])
Date html generated:
2020_05_19-PM-09_37_00
Last ObjectModification:
2019_09_25-PM-03_22_13
Theory : list_0
Home
Index