### Nuprl Lemma : rel_star_functionality_wrt_breqv

`∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 <≡>{T} R2) `` ((R1^*) <≡>{T} (R2^*)))`

Proof

Definitions occuring in Statement :  binrel_eqv: `E <≡>{T} E'` rel_star: `R^*` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` guard: `{T}` prop: `ℙ`
Lemmas referenced :  binrel_le_antisymmetry rel_star_wf rel_star_functionality_wrt_brle binrel_le_weakening binrel_eqv_inversion binrel_eqv_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination because_Cache functionEquality cumulativity universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((R1  <\mequiv{}>\{T\}  R2)  {}\mRightarrow{}  (rel\_star(T;  R1)  <\mequiv{}>\{T\}  rel\_star(T;  R2)))

Date html generated: 2016_05_14-PM-03_55_07
Last ObjectModification: 2015_12_26-PM-06_55_36

Theory : relations2

Home Index