### Nuprl Lemma : lifted-rel_wf

`∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (lifted-rel(R) ∈ (A + B) ⟶ (A + B) ⟶ ℙ)`

Proof

Definitions occuring in Statement :  lifted-rel: `lifted-rel(R)` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` function: `x:A ⟶ B[x]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` lifted-rel: `lifted-rel(R)` isl: `isl(x)` outl: `outl(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` implies: `P `` Q` prop: `ℙ` bfalse: `ff` and: `P ∧ Q` false: `False`
Lemmas referenced :  and_wf true_wf false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality unionElimination thin sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination hypothesis functionEquality applyEquality hypothesisEquality productEquality voidElimination because_Cache unionEquality axiomEquality equalityTransitivity equalitySymmetry cumulativity universeEquality isect_memberEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (lifted-rel(R)  \mmember{}  (A  +  B)  {}\mrightarrow{}  (A  +  B)  {}\mrightarrow{}  \mBbbP{})

Date html generated: 2016_05_15-PM-06_35_23
Last ObjectModification: 2015_12_27-AM-11_55_46

Theory : general

Home Index