### Nuprl Lemma : fpf-single-sub-reflexive

`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[x:A]. ∀[v:B[x]]. ∀[eqa:EqDecider(A)].  x : v ⊆ x : v`

Proof

Definitions occuring in Statement :  fpf-single: `x : v` fpf-sub: `f ⊆ g` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` uimplies: `b supposing a`
Lemmas referenced :  fpf-sub_witness fpf-single_wf deq_wf fpf-sub_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality instantiate hypothesis because_Cache independent_functionElimination isect_memberEquality functionEquality cumulativity universeEquality independent_isectElimination

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[x:A].  \mforall{}[v:B[x]].  \mforall{}[eqa:EqDecider(A)].    x  :  v  \msubseteq{}  x  :  v

Date html generated: 2018_05_21-PM-09_24_43
Last ObjectModification: 2018_02_09-AM-10_20_42

Theory : finite!partial!functions

Home Index