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
Lemmas :  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
\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: 2015_07_17-AM-09_15_30
Last ObjectModification: 2015_01_28-AM-07_54_24

Home Index