Nuprl Lemma : set-equal-nil2

[T:Type]. ∀bs:T List. (set-equal(T;bs;[]) ⇐⇒ ↑null(bs))


Proof




Definitions occuring in Statement :  set-equal: set-equal(T;x;y) null: null(as) nil: [] list: List assert: b uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) uimplies: supposing a or: P ∨ Q cons: [a b] prop: rev_implies:  Q assert: b ifthenelse: if then else fi  btrue: tt top: Top bfalse: ff false: False set-equal: set-equal(T;x;y)
Lemmas referenced :  assert_of_null list-cases nil_wf product_subtype_list assert_witness null_wf set-equal_wf null_nil_lemma set-equal-reflex null_cons_lemma assert_wf list_wf or_wf equal_wf l_member_wf false_wf member_wf cons_wf cons_member nil_member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination dependent_functionElimination unionElimination promote_hyp hypothesis_subsumption sqequalRule independent_functionElimination isect_memberEquality voidElimination voidEquality universeEquality because_Cache inlFormation addLevel impliesFunctionality levelHypothesis andLevelFunctionality impliesLevelFunctionality

Latex:
\mforall{}[T:Type].  \mforall{}bs:T  List.  (set-equal(T;bs;[])  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}null(bs))



Date html generated: 2016_05_14-PM-01_38_24
Last ObjectModification: 2015_12_26-PM-05_28_27

Theory : list_1


Home Index