### Nuprl Lemma : free-word-inv_wf

`∀[X:Type]. ∀[w:free-word(X)].  (free-word-inv(w) ∈ free-word(X))`

Proof

Definitions occuring in Statement :  free-word-inv: `free-word-inv(w)` free-word: `free-word(X)` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` free-word: `free-word(X)` all: `∀x:A. B[x]` prop: `ℙ` implies: `P `` Q` cand: `A c∧ B` free-word-inv: `free-word-inv(w)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` guard: `{T}` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` squash: `↓T` true: `True` equiv_rel: `EquivRel(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` word-equiv: `word-equiv(X;w1;w2)` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` word-rel: `word-rel(X;w1;w2)` append: `as @ bs` so_lambda: so_lambda3 top: `Top` so_apply: `x[s1;s2;s3]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` label: `...\$L... t` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` inverse-letters: `a = -b` or: `P ∨ Q`
Lemmas referenced :  word-equiv-equiv list_wf word-equiv_wf map_wf equal_wf reverse_wf quotient-member-eq equal-wf-base member_wf squash_wf true_wf free-word_wf transitive-reflexive-closure-map word-rel_wf transitive-reflexive-closure_wf subtype_rel_self inverse-letters_wf append_wf cons_wf nil_wf length_wf list_ind_cons_lemma list_ind_nil_lemma length-append exists_wf and_wf iff_weakening_equal free-word-inv-append subtype_rel_list top_wf append_assoc_sq reverse-cons reverse_nil_lemma map_cons_lemma map_nil_lemma decide_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality unionEquality hypothesis promote_hyp lambdaFormation equalityTransitivity equalitySymmetry because_Cache independent_pairFormation sqequalRule lambdaEquality unionElimination inrEquality inlEquality dependent_functionElimination independent_functionElimination independent_isectElimination pointwiseFunctionality pertypeElimination productElimination productEquality applyEquality imageElimination natural_numberEquality imageMemberEquality baseClosed axiomEquality isect_memberEquality universeEquality dependent_pairFormation instantiate rename applyLambdaEquality voidElimination voidEquality dependent_set_memberEquality setElimination cumulativity hyp_replacement

Latex:
\mforall{}[X:Type].  \mforall{}[w:free-word(X)].    (free-word-inv(w)  \mmember{}  free-word(X))

Date html generated: 2020_05_20-AM-08_22_33
Last ObjectModification: 2018_08_21-PM-03_47_45

Theory : free!groups

Home Index