Nuprl Lemma : subtype-deq

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

Proof

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
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B deq: EqDecider(T) so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q prop: rev_implies:  Q guard: {T}
Lemmas referenced :  subtype_rel_dep_function bool_wf subtype_rel_self equal_wf assert_wf all_wf iff_wf deq_wf subtype_rel_wf equal_functionality_wrt_subtype_rel2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality hypothesisEquality applyEquality extract_by_obid isectElimination sqequalRule functionEquality hypothesis independent_isectElimination lambdaFormation because_Cache independent_pairFormation axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry universeEquality independent_functionElimination dependent_functionElimination productElimination

Latex:
\mforall{}[A,B:Type].
(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_04
Last ObjectModification: 2018_09_17-PM-05_40_27

Theory : equality!deciders

Home Index