Nuprl Lemma : subtype_rel_weakening

[A,B:Type].  A ⊆supposing A ≡ B


Proof




Definitions occuring in Statement :  ext-eq: A ≡ B uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  ext-eq: A ≡ B uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q subtype_rel: A ⊆B prop:
Lemmas referenced :  and_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin hypothesis axiomEquality lemma_by_obid isectElimination hypothesisEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[A,B:Type].    A  \msubseteq{}r  B  supposing  A  \mequiv{}  B



Date html generated: 2016_05_13-PM-03_19_11
Last ObjectModification: 2015_12_26-AM-09_07_50

Theory : subtype_0


Home Index