### Nuprl Lemma : subtype_bar2

`∀[A,B:Type].  bar(A) ⊆r bar(B) supposing (A ⊆r B) ∧ (value-type(A) ∨ (A ⊆r Base)) ∧ (value-type(B) ∨ (B ⊆r Base))`

Proof

Definitions occuring in Statement :  bar: `bar(T)` value-type: `value-type(T)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` or: `P ∨ Q` and: `P ∧ Q` base: `Base` universe: `Type`
Definitions unfolded in proof :  bar: `bar(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` subtype_rel: `A ⊆r B` prop: `ℙ`
Lemmas referenced :  base_wf value-type_wf or_wf subtype_rel_wf and_wf subtype_rel_partial
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination hypothesisEquality independent_isectElimination hypothesis axiomEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[A,B:Type].
bar(A)  \msubseteq{}r  bar(B)
supposing  (A  \msubseteq{}r  B)  \mwedge{}  (value-type(A)  \mvee{}  (A  \msubseteq{}r  Base))  \mwedge{}  (value-type(B)  \mvee{}  (B  \msubseteq{}r  Base))

Date html generated: 2016_05_15-PM-10_03_46
Last ObjectModification: 2016_01_05-PM-06_26_46

Theory : bar!type

Home Index