Nuprl Lemma : rel-immediate_functionality_wrt_breqv

[T:Type]. ∀[R,Q:T ⟶ T ⟶ ℙ].  ((R <≡>{T} Q)  (R! <≡>{T} Q!))


Proof




Definitions occuring in Statement :  rel-immediate: R! binrel_eqv: E <≡>{T} E' uall: [x:A]. B[x] prop: implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  binrel_eqv: E <≡>{T} E'
Lemmas referenced :  rel-immediate_functionality_wrt_iff
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut lemma_by_obid hypothesis

Latex:
\mforall{}[T:Type].  \mforall{}[R,Q:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((R  <\mequiv{}>\{T\}  Q)  {}\mRightarrow{}  (R!  <\mequiv{}>\{T\}  Q!))



Date html generated: 2016_05_15-PM-04_53_36
Last ObjectModification: 2015_12_27-PM-02_31_58

Theory : general


Home Index