Nuprl Lemma : mrec-induction2-ext
∀L:MutualRectypeSpec. ∀[P:mobj(L) ⟶ TYPE]. (mrecind(L;x.P[x]) ⇒ (∀x:mobj(L). P[x]))
Proof
Definitions occuring in Statement :
mrecind: mrecind(L;x.P[x]),
mobj: mobj(L),
mrec_spec: MutualRectypeSpec,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
member: t ∈ T,
mobj-kind: mobj-kind(x),
pi1: fst(t),
mobj-label: mobj-label(x),
prec-label: prec-label(x),
mobj-data: mobj-data(x),
pi2: snd(t),
mobj-tuple: mobj-tuple(x),
prec-tuple: prec-tuple(x),
mrec-spec: mrec-spec(L;lbl;p),
nil: [],
it: ⋅,
genrec-ap: genrec-ap,
let: let,
mrec-induction2,
mrec-induction,
mobj-ext,
prec-induction-ext
Lemmas referenced :
mrec-induction2,
mrec-induction,
mobj-ext,
prec-induction-ext
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}L:MutualRectypeSpec. \mforall{}[P:mobj(L) {}\mrightarrow{} TYPE]. (mrecind(L;x.P[x]) {}\mRightarrow{} (\mforall{}x:mobj(L). P[x]))
Date html generated:
2019_06_20-PM-02_16_18
Last ObjectModification:
2019_03_25-PM-11_28_29
Theory : tuples
Home
Index