Nuprl Lemma : mkterm-one-one
∀[Op:Type]. ∀[f,g:Op]. ∀[as,bs:(varname() List × term(Op)) List].
((mkterm(f;as) = mkterm(g;bs) ∈ term(Op)) ⇒ {(f = g ∈ Op) ∧ (as = bs ∈ ((varname() List × term(Op)) List))})
Proof
Definitions occuring in Statement :
mkterm: mkterm(opr;bts),
term: term(opr),
varname: varname(),
list: T List,
uall: ∀[x:A]. B[x],
guard: {T},
implies: P ⇒ Q,
and: P ∧ Q,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ext-eq: A ≡ B,
and: P ∧ Q,
implies: P ⇒ Q,
uimplies: b supposing a,
guard: {T},
mkterm: mkterm(opr;bts),
coterm-fun: coterm-fun(opr;T),
prop: ℙ,
uiff: uiff(P;Q),
so_lambda: λ2x.t[x],
so_apply: x[s],
pi2: snd(t),
pi1: fst(t),
cand: A c∧ B
Lemmas referenced :
term-ext,
equal_functionality_wrt_subtype_rel2,
term_wf,
coterm-fun_wf,
mkterm_wf,
list_wf,
varname_wf,
istype-universe,
inr-one-one,
not_wf,
equal-wf-T-base,
pi2_wf,
pi1_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
productElimination,
lambdaFormation_alt,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination,
independent_functionElimination,
equalityIstype,
universeIsType,
because_Cache,
productEquality,
instantiate,
universeEquality,
setEquality,
baseClosed,
independent_pairEquality,
applyLambdaEquality,
sqequalRule,
lambdaEquality_alt,
inhabitedIsType,
independent_pairFormation
Latex:
\mforall{}[Op:Type]. \mforall{}[f,g:Op]. \mforall{}[as,bs:(varname() List \mtimes{} term(Op)) List].
((mkterm(f;as) = mkterm(g;bs)) {}\mRightarrow{} \{(f = g) \mwedge{} (as = bs)\})
Date html generated:
2020_05_19-PM-09_53_42
Last ObjectModification:
2020_03_10-PM-03_45_22
Theory : terms
Home
Index