### Nuprl Lemma : permutation-equiv

`∀[A:Type]. EquivRel(A List)(permutation(A;_1;_2))`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` list: `T List` equiv_rel: `EquivRel(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` member: `t ∈ T` sym: `Sym(T;x,y.E[x; y])` implies: `P `` Q` prop: `ℙ` trans: `Trans(T;x,y.E[x; y])` uimplies: `b supposing a`
Lemmas referenced :  list_wf permutation_inversion permutation_wf permutation_transitivity permutation_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache dependent_functionElimination independent_functionElimination universeEquality independent_isectElimination

Latex:
\mforall{}[A:Type].  EquivRel(A  List)(permutation(A;\$_{1}\$;\$_{2}\$))

Date html generated: 2016_05_14-PM-02_19_24
Last ObjectModification: 2015_12_26-PM-04_28_31

Theory : list_1

Home Index