### Nuprl Lemma : test-change-equality

`∀[L1:ℕ List]. ∀[L2:ℤ List].  ((L1 = L2 ∈ (ℤ List)) `` (L1 = L2 ∈ (ℕ List)))`

Proof

Definitions occuring in Statement :  list: `T List` nat: `ℕ` uall: `∀[x:A]. B[x]` implies: `P `` Q` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` subtype_rel: `A ⊆r B` uimplies: `b supposing a` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]`
Lemmas referenced :  list_subtype_base nat_wf set_subtype_base le_wf istype-int int_subtype_base list_wf change-equality-type respects-equality-list subtype-base-respects-equality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :equalityIstype,  because_Cache cut hypothesisEquality applyEquality introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination sqequalRule intEquality Error :lambdaEquality_alt,  closedConclusion natural_numberEquality sqequalBase equalitySymmetry Error :universeIsType,  independent_functionElimination dependent_functionElimination equalityTransitivity

Latex:
\mforall{}[L1:\mBbbN{}  List].  \mforall{}[L2:\mBbbZ{}  List].    ((L1  =  L2)  {}\mRightarrow{}  (L1  =  L2))

Date html generated: 2019_06_20-PM-01_49_13
Last ObjectModification: 2018_11_29-PM-05_52_22

Theory : list_1

Home Index