Nuprl Lemma : lnk-decls-compatible
∀[l1,l2:IdLnk]. ∀[d1,d2:tg:Id fp-> Type]. lnk-decl(l1;d1) || lnk-decl(l2;d2) supposing (l1 = l2 ∈ IdLnk) ⇒ d1 || d2
Proof
Definitions occuring in Statement :
lnk-decl: lnk-decl(l;dt),
fpf-compatible: f || g,
fpf: a:A fp-> B[a],
Kind-deq: KindDeq,
Knd: Knd,
IdLnk: IdLnk,
id-deq: IdDeq,
Id: Id,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T
Lemmas :
subtype_base_sq,
IdLnk_wf,
product_subtype_base,
Id_wf,
atom2_subtype_base,
assert_wf,
fpf-dom_wf,
Knd_wf,
Kind-deq_wf,
lnk-decl_wf-hasloc,
subtype-fpf3,
hasloc_wf,
ldst_wf,
top_wf,
strong-subtype-set2,
subtype_top,
set_wf,
assert-deq-member,
map_wf,
rcv_wf,
member_map,
union_subtype_base,
fpf_ap_pair_lemma,
tag_rcv_lemma,
and_wf,
equal_wf,
tagof_wf,
isrcv_rcv_lemma,
isrcv_wf,
l_member_wf,
id-deq_wf,
rcv_one_one
\mforall{}[l1,l2:IdLnk]. \mforall{}[d1,d2:tg:Id fp-> Type].
lnk-decl(l1;d1) || lnk-decl(l2;d2) supposing (l1 = l2) {}\mRightarrow{} d1 || d2
Date html generated:
2015_07_17-AM-11_16_13
Last ObjectModification:
2015_02_04-PM-05_06_05
Home
Index