### Nuprl Lemma : free-dl-generator_wf

`∀[X:Type]. ∀[x:X].  (free-dl-generator(x) ∈ free-dl-type(X))`

Proof

Definitions occuring in Statement :  free-dl-generator: `free-dl-generator(x)` free-dl-type: `free-dl-type(X)` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` free-dl-generator: `free-dl-generator(x)` subtype_rel: `A ⊆r B` free-dl-type: `free-dl-type(X)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a`
Lemmas referenced :  cons_wf list_wf nil_wf subtype_quotient dlattice-eq_wf dlattice-eq-equiv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis applyEquality lambdaEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[X:Type].  \mforall{}[x:X].    (free-dl-generator(x)  \mmember{}  free-dl-type(X))

Date html generated: 2017_02_21-AM-09_54_48
Last ObjectModification: 2017_01_22-PM-07_46_48

Theory : lattices

Home Index