Nuprl Lemma : very-dep-fun-eta

[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])].  (f L,b. (f b)) ∈ very-dep-fun(A;B;a,b.C[a;b]\000C))


Proof




Definitions occuring in Statement :  very-dep-fun: very-dep-fun(A;B;a,b.C[a; b]) uall: [x:A]. B[x] so_apply: x[s1;s2] apply: a lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T very-dep-fun: very-dep-fun(A;B;a,b.C[a; b]) all: x:A. B[x] decidable: Dec(P) or: P ∨ Q nat: vdf: vdf(A;B;a,b.C[a; b];n) implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb ifthenelse: if then else fi  assert: b false: False not: ¬A rev_implies:  Q iff: ⇐⇒ Q satisfiable_int_formula: satisfiable_int_formula(fmla) prop: so_apply: x[s1;s2] subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] ge: i ≥  lt_int: i <j subtract: m
Lemmas referenced :  decidable__le istype-le lt_int_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf istype-less_than full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf eta_conv list_wf length_wf_nat set_subtype_base le_wf int_subtype_base very-dep-fun_wf istype-universe nat_properties ge_wf subtract-1-ge-0 istype-nat equal-wf-base le_int_wf bnot_wf uiff_transitivity assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int not_wf istype-assert istype-void bool_cases iff_transitivity assert_of_bnot length_wf vdf-eq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution isect_memberEquality_alt extract_by_obid dependent_functionElimination thin natural_numberEquality hypothesisEquality hypothesis unionElimination dependent_set_memberEquality_alt isectElimination because_Cache sqequalRule inhabitedIsType lambdaFormation_alt equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination dependent_pairFormation_alt equalityIstype promote_hyp instantiate cumulativity independent_functionElimination voidElimination approximateComputation lambdaEquality_alt int_eqEquality Error :memTop,  independent_pairFormation universeIsType functionExtensionality_alt applyEquality setIsType productEquality intEquality baseClosed sqequalBase axiomEquality isectIsTypeImplies functionIsType universeEquality setElimination rename intWeakElimination functionIsTypeImplies baseApply closedConclusion dependentIntersection_memberEquality dependentIntersectionEqElimination functionExtensionality setEquality applyLambdaEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].  \mforall{}[f:very-dep-fun(A;B;a,b.C[a;b])].    (f  =  (\mlambda{}L,b.  (f  L  b)))



Date html generated: 2020_05_19-PM-09_40_33
Last ObjectModification: 2020_03_10-PM-00_32_13

Theory : co-recursion-2


Home Index