Nuprl Lemma : copath-hd_wf

[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)].
  copath-hd(p) ∈ coW-dom(a.B[a];w) supposing 0 < copath-length(p)


Proof




Definitions occuring in Statement :  copath-hd: copath-hd(p) copath-length: copath-length(p) copath: copath(a.B[a];w) coW-dom: coW-dom(a.B[a];w) coW: coW(A;a.B[a]) less_than: a < b uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a copath-hd: copath-hd(p) copath: copath(a.B[a];w) pi1: fst(t) pi2: snd(t) copath-length: copath-length(p) coPath: coPath(a.B[a];w;n) prop: so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B nat: false: False guard: {T} all: x:A. B[x] implies:  Q or: P ∨ Q sq_type: SQType(T) uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  btrue: tt iff: ⇐⇒ Q not: ¬A rev_implies:  Q bfalse: ff
Lemmas referenced :  less_than_wf copath-length_wf nat_wf copath_wf coW_wf eq_int_wf less_than_transitivity1 le_weakening less_than_irreflexivity assert_wf bnot_wf not_wf equal-wf-T-base bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert assert_of_eq_int eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin hypothesis axiomEquality equalityTransitivity equalitySymmetry extract_by_obid isectElimination natural_numberEquality hypothesisEquality lambdaEquality applyEquality setElimination rename isect_memberEquality because_Cache instantiate cumulativity functionEquality universeEquality independent_isectElimination dependent_functionElimination independent_functionElimination voidElimination intEquality baseClosed spreadEquality unionElimination independent_pairFormation lambdaFormation impliesFunctionality

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p:copath(a.B[a];w)].
    copath-hd(p)  \mmember{}  coW-dom(a.B[a];w)  supposing  0  <  copath-length(p)



Date html generated: 2018_07_25-PM-01_39_41
Last ObjectModification: 2018_06_01-AM-11_27_14

Theory : co-recursion


Home Index