### Nuprl Lemma : deq-all-disjoint_wf

`∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[ass:A List List]. ∀[bs:A List].  (deq-all-disjoint(eq;ass;bs) ∈ 𝔹)`

Proof

Definitions occuring in Statement :  deq-all-disjoint: `deq-all-disjoint(eq;ass;bs)` list: `T List` deq: `EqDecider(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  deq-all-disjoint: `deq-all-disjoint(eq;ass;bs)` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]`
Lemmas referenced :  bl-all_wf list_wf deq-disjoint_wf l_member_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality setElimination rename setEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[ass:A  List  List].  \mforall{}[bs:A  List].    (deq-all-disjoint(eq;ass;bs)  \mmember{}  \mBbbB{})

Date html generated: 2016_05_14-PM-03_24_06
Last ObjectModification: 2015_12_26-PM-06_21_30

Theory : decidable!equality

Home Index