Nuprl Lemma : implies-vdf-eq-append1
∀A,B:Type. ∀C:A ⟶ B ⟶ Type. ∀f:very-dep-fun(A;B;a,b.C[a;b]). ∀L:(a:A × b:B × C[a;b]) List. ∀a:A. ∀b:B. ∀c:Top.
(vdf-eq(A;f;L) ⇒ (a = (f L b) ∈ A) ⇒ vdf-eq(A;f;L @ [<a, b, c>]))
Proof
Definitions occuring in Statement :
very-dep-fun: very-dep-fun(A;B;a,b.C[a; b]),
vdf-eq: vdf-eq(A;f;L),
append: as @ bs,
cons: [a / b],
nil: [],
list: T List,
top: Top,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
pair: <a, b>,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
so_apply: x[s1;s2],
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s],
so_lambda: λ2x y.t[x; y],
prop: ℙ
Lemmas referenced :
very-dep-fun-subtype,
vdf-eq-append1,
subtype_rel_list,
top_wf,
subtype_rel_product,
vdf-eq-witness,
vdf-eq_wf,
istype-top,
list_wf,
very-dep-fun_wf,
istype-universe
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_functionElimination,
Error :memTop,
applyEquality,
productEquality,
independent_isectElimination,
sqequalRule,
lambdaEquality_alt,
inhabitedIsType,
universeIsType,
because_Cache,
dependentIntersection_memberEquality,
axiomEquality,
equalityIstype,
dependent_set_memberEquality_alt,
functionIsType,
instantiate,
universeEquality
Latex:
\mforall{}A,B:Type. \mforall{}C:A {}\mrightarrow{} B {}\mrightarrow{} Type. \mforall{}f:very-dep-fun(A;B;a,b.C[a;b]). \mforall{}L:(a:A \mtimes{} b:B \mtimes{} C[a;b]) List. \mforall{}a:A.
\mforall{}b:B. \mforall{}c:Top.
(vdf-eq(A;f;L) {}\mRightarrow{} (a = (f L b)) {}\mRightarrow{} vdf-eq(A;f;L @ [<a, b, c>]))
Date html generated:
2020_05_19-PM-09_41_03
Last ObjectModification:
2020_03_09-PM-01_55_13
Theory : co-recursion-2
Home
Index