Nuprl Lemma : decidable__equal

{

a,b:Id. Dec(a = b) }

{ Proof }

Definitions occuring in Statement : Id: Id, decidable: Dec(P), all:

x:A. B[x], equal: s = t
Definitions : eq_id: a = b, limited-type: LimitedType, lambda:

x.A[x], member: t

T, rev_implies: P

Q, uiff: uiff(P;Q), uimplies: b supposing a, isect:

x:A. B[x], uall:

[x:A]. B[x], iff: P

Q, and: P

Q, implies: P

Q, product: x:A

B[x], assert:

b, prop:

, universe: Type, so_lambda:

x.t[x], all:

x:A. B[x], function: x:A

B[x], decidable: Dec(P), equal: s = t, Id: Id, Auto: Error :Auto, CollapseTHENA: Error :CollapseTHENA, tactic: Error :tactic, divides: b | a, assoced: a ~ b, set_leq: a

b, set_lt: a <p b, grp_lt: a < b, cand: A c

B, l_member: (x

l), l_contains: A

B, inject: Inj(A;B;f), reducible: reducible(a), prime: prime(a), squash:

T, l_disjoint: l_disjoint(T;l1;l2), l_exists: (

x

L. P[x]), l_all: (

x

L.P[x]), apply: f a, infix_ap: x f y, fun-connected: y is f*(x), qle: r

s, qless: r < s, q-rel: q-rel(r;x), exists:

x:A. B[x], i-finite: i-finite(I), i-closed: i-closed(I), p-outcome: Outcome, fset-member: a

s, fset-closed: (s closed under fs), f-subset: xs

ys
Lemmas : decidable__assert, all_functionality_wrt_iff, decidable_functionality, iff_weakening_uiff, uiff_inversion, assert-eq-id, decidable_wf, assert_wf, eq_id_wf, Id_wf

\mforall{}a,b:Id. Dec(a = b) Date html generated: 2011_08_10-AM-07_47_53 Last ObjectModification: 2010_11_29-PM-11_50_42 Home Index