Nuprl Lemma : pi-subst-aux_wf
∀[p:pi_term()]. (pi-subst-aux(p) ∈ (Name List) ─→ ((Name × Name) List) ─→ pi_term())
Proof
Definitions occuring in Statement :
pi-subst-aux: pi-subst-aux(p),
pi_term: pi_term(),
name: Name,
list: T List,
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ─→ B[x],
product: x:A × B[x]
Lemmas :
pi_term_ind_wf_simple,
list_wf,
name_wf,
pi_term_wf,
pizero_wf,
pi_prefix_ind_wf_simple,
picomm_wf,
pisend_wf,
name-subst_wf,
deq-member_wf,
name-deq_wf,
bool_wf,
eqtt_to_assert,
assert-deq-member,
pircv_wf,
maybe-new_wf,
append_wf,
pi-names_wf,
not_wf,
l_member_wf,
cons_wf,
filter_wf5,
bnot_wf,
name_eq_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
pi_prefix_wf,
pioption_wf,
pipar_wf,
pirep_wf,
pinew_wf
Latex:
\mforall{}[p:pi\_term()]. (pi-subst-aux(p) \mmember{} (Name List) {}\mrightarrow{} ((Name \mtimes{} Name) List) {}\mrightarrow{} pi\_term())
Date html generated:
2015_07_23-AM-11_33_38
Last ObjectModification:
2015_01_29-AM-00_54_35
Home
Index