Nuprl Lemma : urefl_functionality_wrt_iff

[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  (R[x;y] ⇐⇒ R'[x;y]))  (UniformlyRefl(T;x,y.R[x;y]) ⇐⇒ UniformlyRefl(T;x,y.R'[x;y])))


Proof




Definitions occuring in Statement :  urefl: UniformlyRefl(T;x,y.E[x; y]) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] iff: ⇐⇒ Q implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  urefl: UniformlyRefl(T;x,y.E[x; y]) uall: [x:A]. B[x] implies:  Q iff: ⇐⇒ Q and: P ∧ Q member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s1;s2] so_apply: x[s] rev_implies:  Q guard: {T}
Lemmas referenced :  uall_wf iff_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  lambdaFormation independent_pairFormation Error :universeIsType,  hypothesisEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin lambdaEquality applyEquality hypothesis Error :inhabitedIsType,  Error :functionIsType,  universeEquality because_Cache productElimination independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R,R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}[x,y:T].    (R[x;y]  \mLeftarrow{}{}\mRightarrow{}  R'[x;y]))
    {}\mRightarrow{}  (UniformlyRefl(T;x,y.R[x;y])  \mLeftarrow{}{}\mRightarrow{}  UniformlyRefl(T;x,y.R'[x;y])))



Date html generated: 2019_06_20-PM-00_28_44
Last ObjectModification: 2018_09_26-AM-11_46_33

Theory : rel_1


Home Index