Nuprl Lemma : strong-subtype_transitivity

[A,B,C:Type].  (strong-subtype(A;C)) supposing (strong-subtype(B;C) and strong-subtype(A;B))


Proof




Definitions occuring in Statement :  strong-subtype: strong-subtype(A;B) uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a implies:  Q guard: {T} strong-subtype: strong-subtype(A;B) cand: c∧ B subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] exists: x:A. B[x] prop: all: x:A. B[x]
Lemmas referenced :  strong-subtype-implies subtype_rel_transitivity exists_wf equal_wf strong-subtype_witness strong-subtype_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis productElimination independent_isectElimination independent_pairFormation lambdaEquality setEquality sqequalRule applyEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality setElimination rename dependent_functionElimination

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



Date html generated: 2019_06_20-PM-00_27_52
Last ObjectModification: 2018_09_12-PM-11_28_24

Theory : subtype_1


Home Index