Nuprl Lemma : strong-subtype-eq3

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


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}
Lemmas referenced :  strong-subtype-eq2
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep hypothesis

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



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

Theory : subtype_1


Home Index