### Nuprl Lemma : permr_weakening

`∀T:Type. ∀as,bs:T List.  ((as = bs ∈ (T List)) `` (as ≡(T) bs))`

Proof

Definitions occuring in Statement :  permr: `as ≡(T) bs` list: `T List` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  permr: `as ≡(T) bs` all: `∀x:A. B[x]` implies: `P `` Q` cand: `A c∧ B` member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` true: `True` prop: `ℙ` exists: `∃x:A. B[x]` sym_grp: `Sym(n)` so_lambda: `λ2x.t[x]` perm: `Perm(T)` subtype_rel: `A ⊆r B` uimplies: `b supposing a` ge: `i ≥ j ` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` nat: `ℕ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` top: `Top` so_apply: `x[s]` id_perm: `id_perm()` mk_perm: `mk_perm(f;b)` perm_f: `p.f` pi1: `fst(t)` identity: `Id`
Lemmas referenced :  less_than_wf and_wf squash_wf int_formula_prop_eq_lemma intformeq_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_formula_prop_not_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformnot_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf satisfiable-full-omega-tt le_wf nat_properties length_wf_nat lelt_wf decidable__le int_seg_properties non_neg_length perm_f_wf select_wf all_wf int_seg_wf id_perm_wf list_wf equal_wf length_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination lemma_by_obid isectElimination because_Cache hypothesis hypothesisEquality equalitySymmetry natural_numberEquality imageMemberEquality baseClosed independent_pairFormation dependent_pairFormation dependent_functionElimination equalityTransitivity cumulativity setElimination rename independent_isectElimination productElimination dependent_set_memberEquality unionElimination setEquality intEquality int_eqEquality isect_memberEquality voidElimination voidEquality computeAll universeEquality

Latex:
\mforall{}T:Type.  \mforall{}as,bs:T  List.    ((as  =  bs)  {}\mRightarrow{}  (as  \mequiv{}(T)  bs))

Date html generated: 2016_05_16-AM-07_32_31
Last ObjectModification: 2016_01_16-PM-11_09_33

Theory : perms_2

Home Index