Nuprl Lemma : perm_f_b_cancel

T:Type. ∀p:Perm(T). ∀x:T.  ((p.f (p.b x)) x ∈ T)


Proof




Definitions occuring in Statement :  perm: Perm(T) perm_b: p.b perm_f: p.f all: x:A. B[x] apply: a universe: Type equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T inv_funs: InvFuns(A;B;f;g) and: P ∧ Q uall: [x:A]. B[x] true: True compose: g tidentity: Id{T} identity: Id squash: T prop: subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  perm_properties istype-universe perm_wf equal_wf squash_wf true_wf subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis productElimination isectElimination universeIsType universeEquality natural_numberEquality sqequalRule applyEquality lambdaEquality_alt imageElimination equalityTransitivity equalitySymmetry inhabitedIsType imageMemberEquality baseClosed instantiate independent_isectElimination independent_functionElimination

Latex:
\mforall{}T:Type.  \mforall{}p:Perm(T).  \mforall{}x:T.    ((p.f  (p.b  x))  =  x)



Date html generated: 2019_10_16-PM-01_00_36
Last ObjectModification: 2018_10_08-AM-10_57_42

Theory : perms_2


Home Index