Nuprl Lemma : EquatePairs_wf

[x,y,n,m:Base].
  (EquatePairs(x;n;y;m) ∈ Type) supposing ((¬(n m ∈ Base)) and (x m ∈ Base)) and (y n ∈ Base)))


Proof




Definitions occuring in Statement :  EquatePairs: EquatePairs(x;n;y;m) uimplies: supposing a uall: [x:A]. B[x] not: ¬A member: t ∈ T base: Base universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a EquatePairs: EquatePairs(x;n;y;m) so_lambda: λ2y.t[x; y] prop: or: P ∨ Q and: P ∧ Q so_apply: x[s1;s2] not: ¬A implies:  Q false: False all: x:A. B[x] cand: c∧ B guard: {T}
Lemmas referenced :  pertype_wf equal-wf-base base_wf istype-void istype-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule Error :lambdaEquality_alt,  unionEquality hypothesis hypothesisEquality productEquality because_Cache Error :inhabitedIsType,  independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry Error :functionIsType,  Error :equalityIstype,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :lambdaFormation_alt,  unionElimination Error :inlFormation_alt,  Error :unionIsType,  Error :productIsType,  productElimination Error :inrFormation_alt,  independent_pairFormation independent_functionElimination voidElimination

Latex:
\mforall{}[x,y,n,m:Base].    (EquatePairs(x;n;y;m)  \mmember{}  Type)  supposing  ((\mneg{}(n  =  m))  and  (\mneg{}(x  =  m))  and  (\mneg{}(y  =  n)))



Date html generated: 2019_06_20-PM-02_44_14
Last ObjectModification: 2019_01_13-PM-03_28_12

Theory : num_thy_1


Home Index