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