Nuprl Lemma : l_disjoint-symmetry

`∀[T:Type]. ∀[a,b:T List].  uiff(l_disjoint(T;b;a);l_disjoint(T;a;b))`

Proof

Definitions occuring in Statement :  l_disjoint: `l_disjoint(T;l1;l2)` list: `T List` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` l_disjoint: `l_disjoint(T;l1;l2)` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` cand: `A c∧ B` false: `False` prop: `ℙ`
Lemmas referenced :  and_wf l_member_wf l_disjoint_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation sqequalHypSubstitution lambdaFormation hypothesis dependent_functionElimination thin hypothesisEquality independent_functionElimination productElimination voidElimination lemma_by_obid isectElimination sqequalRule lambdaEquality because_Cache independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[a,b:T  List].    uiff(l\_disjoint(T;b;a);l\_disjoint(T;a;b))

Date html generated: 2016_05_14-AM-07_55_41
Last ObjectModification: 2015_12_26-PM-04_49_39

Theory : list_1

Home Index