Nuprl Lemma : cancel_shift

[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].
  (Cancel(A;A;opa)) supposing (Cancel(B;B;opb) and FunThru2op(A;B;opa;opb;f) and Inj(A;B;f))


Definitions occuring in Statement :  cancel: Cancel(T;S;op) fun_thru_2op: FunThru2op(A;B;opa;opb;f) inject: Inj(A;B;f) uimplies: supposing a uall: [x:A]. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a cancel: Cancel(T;S;op) fun_thru_2op: FunThru2op(A;B;opa;opb;f) inject: Inj(A;B;f) prop: infix_ap: y squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q implies:  Q all: x:A. B[x]
Lemmas referenced :  equal_wf cancel_wf fun_thru_2op_wf inject_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis extract_by_obid isectElimination thin cumulativity hypothesisEquality applyEquality functionExtensionality sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry functionEquality universeEquality lambdaEquality imageElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination dependent_functionElimination

\mforall{}[A,B:Type].  \mforall{}[opa:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].  \mforall{}[opb:B  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[f:A  {}\mrightarrow{}  B].
    (Cancel(A;A;opa))  supposing  (Cancel(B;B;opb)  and  FunThru2op(A;B;opa;opb;f)  and  Inj(A;B;f))

Date html generated: 2017_10_01-AM-08_13_06
Last ObjectModification: 2017_02_28-PM-01_57_25

Theory : gen_algebra_1

Home Index