Nuprl Lemma : strong-subtype-eq4

[A,B:Type]. ∀[b:B]. ∀[a:A].  {b a ∈ supposing a ∈ A} supposing strong-subtype(B;A)


Proof




Definitions occuring in Statement :  strong-subtype: strong-subtype(A;B) uimplies: supposing a uall: [x:A]. B[x] guard: {T} universe: Type equal: t ∈ T
Definitions unfolded in proof :  guard: {T} uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: subtype_rel: A ⊆B strong-subtype: strong-subtype(A;B) cand: c∧ B
Lemmas referenced :  equal_wf strong-subtype_wf strong-subtype-eq2
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality productElimination isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry universeEquality independent_isectElimination

Latex:
\mforall{}[A,B:Type].  \mforall{}[b:B].  \mforall{}[a:A].    \{b  =  a  supposing  b  =  a\}  supposing  strong-subtype(B;A)



Date html generated: 2016_05_13-PM-04_11_37
Last ObjectModification: 2015_12_26-AM-11_21_21

Theory : subtype_1


Home Index