Nuprl Lemma : permutation-cons2

`∀[A:Type]. ∀x:A. ∀L1,L2:A List.  (permutation(A;L1;L2) `` permutation(A;[x / L1];[x / L2]))`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` cons: `[a / b]` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` exists: `∃x:A. B[x]` cand: `A c∧ B` append: `as @ bs` list_ind: list_ind nil: `[]` it: `⋅` cons: `[a / b]` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  permutation_wf list_wf permutation-cons cons_wf nil_wf and_wf equal_wf append_wf exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis universeEquality dependent_functionElimination productElimination independent_functionElimination dependent_pairFormation sqequalRule because_Cache independent_pairFormation lambdaEquality

Latex:
\mforall{}[A:Type].  \mforall{}x:A.  \mforall{}L1,L2:A  List.    (permutation(A;L1;L2)  {}\mRightarrow{}  permutation(A;[x  /  L1];[x  /  L2]))

Date html generated: 2016_05_14-PM-02_31_53
Last ObjectModification: 2015_12_26-PM-04_22_55

Theory : list_1

Home Index