Nuprl Lemma : subtype-fpf3

[A1,A2:Type]. ∀[B1:A1 ⟶ Type]. ∀[B2:A2 ⟶ Type].
  (a:A1 fp-> B1[a] ⊆a:A2 fp-> B2[a]) supposing ((∀a:A1. (B1[a] ⊆B2[a])) and strong-subtype(A1;A2))


Definitions occuring in Statement :  fpf: a:A fp-> B[a] strong-subtype: strong-subtype(A;B) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a subtype_rel: A ⊆B member: t ∈ T implies:  Q guard: {T} fpf: a:A fp-> B[a] strong-subtype: strong-subtype(A;B) cand: c∧ B prop: so_apply: x[s] so_lambda: λ2x.t[x] all: x:A. B[x]
Lemmas referenced :  strong-subtype-implies subtype_rel_list l_member_wf fpf_wf all_wf subtype_rel_wf strong-subtype_wf strong-subtype-l_member-type strong-subtype-l_member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis productElimination dependent_pairEquality applyEquality independent_isectElimination sqequalRule functionExtensionality setEquality functionEquality setElimination rename cumulativity universeEquality because_Cache dependent_functionElimination dependent_set_memberEquality equalityTransitivity equalitySymmetry

\mforall{}[A1,A2:Type].  \mforall{}[B1:A1  {}\mrightarrow{}  Type].  \mforall{}[B2:A2  {}\mrightarrow{}  Type].
    (a:A1  fp->  B1[a]  \msubseteq{}r  a:A2  fp->  B2[a])  supposing 
          ((\mforall{}a:A1.  (B1[a]  \msubseteq{}r  B2[a]))  and 

Date html generated: 2018_05_21-PM-09_17_07
Last ObjectModification: 2018_02_09-AM-10_16_23

Theory : finite!partial!functions

Home Index