Nuprl Lemma : assert-isrcvl
∀[k:Knd]. ∀[l:IdLnk]. uiff(↑isrcvl(l;k);(↑isrcv(k)) ∧ (lnk(k) = l ∈ IdLnk))
Proof
Definitions occuring in Statement :
isrcvl: isrcvl(l;k),
lnk: lnk(k),
isrcv: isrcv(k),
Knd: Knd,
IdLnk: IdLnk,
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
equal: s = t ∈ T
Lemmas :
assert_witness,
assert_wf,
isrcv_wf,
bool_wf,
eqtt_to_assert,
eq_lnk_wf,
lnk_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert-eq-lnk,
IdLnk_wf,
Knd_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
false_wf
\mforall{}[k:Knd]. \mforall{}[l:IdLnk]. uiff(\muparrow{}isrcvl(l;k);(\muparrow{}isrcv(k)) \mwedge{} (lnk(k) = l))
Date html generated:
2015_07_17-AM-09_12_59
Last ObjectModification:
2015_01_28-AM-07_55_52
Home
Index