Nuprl Lemma : inverse-inverse-letters
∀[X:Type]. ∀[a,b,c:X + X]. (a = -b ⇒ c = -a ⇒ (c = b ∈ (X + X)))
Proof
Definitions occuring in Statement :
inverse-letters: a = -b,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
union: left + right,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
inverse-letters: a = -b,
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
isl: isl(x),
prop: ℙ,
not: ¬A,
false: False,
outr: outr(x),
uimplies: b supposing a,
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
bfalse: ff,
assert: ↑b,
btrue: tt,
true: True,
outl: outl(x)
Lemmas referenced :
btrue_wf,
bfalse_wf,
and_wf,
equal_wf,
isl_wf,
btrue_neq_bfalse,
outr_wf,
assert_wf,
bnot_wf,
outl_wf,
inverse-letters_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
unionElimination,
sqequalRule,
extract_by_obid,
hypothesis,
equalityTransitivity,
equalitySymmetry,
dependent_set_memberEquality,
independent_pairFormation,
isectElimination,
unionEquality,
hypothesisEquality,
applyLambdaEquality,
setElimination,
rename,
independent_functionElimination,
voidElimination,
independent_isectElimination,
promote_hyp,
hyp_replacement,
natural_numberEquality,
inlEquality,
inrEquality,
cumulativity,
lambdaEquality,
dependent_functionElimination,
axiomEquality,
isect_memberEquality,
because_Cache,
universeEquality
Latex:
\mforall{}[X:Type]. \mforall{}[a,b,c:X + X]. (a = -b {}\mRightarrow{} c = -a {}\mRightarrow{} (c = b))
Date html generated:
2017_01_19-PM-02_49_13
Last ObjectModification:
2017_01_14-PM-04_00_28
Theory : free!groups
Home
Index