Nuprl Lemma : subtype_rel-deq

[A,B:Type].  (EqDecider(B) ⊆EqDecider(A)) supposing ((∀x,y:A.  ((x y ∈ B)  (x y ∈ A))) and (A ⊆B))


Definitions occuring in Statement :  deq: EqDecider(T) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] all: x:A. B[x] implies:  Q universe: Type equal: t ∈ T
Lemmas referenced :  subtype-deq
Rules used in proof :  cut introduction extract_by_obid hypothesis

    (EqDecider(B)  \msubseteq{}r  EqDecider(A))  supposing  ((\mforall{}x,y:A.    ((x  =  y)  {}\mRightarrow{}  (x  =  y)))  and  (A  \msubseteq{}r  B))

Date html generated: 2019_06_20-PM-00_32_05
Last ObjectModification: 2018_09_17-PM-05_40_26

Theory : equality!deciders

Home Index