Nuprl Lemma : coSet-subtype-corec

coSet{i:l} ⊆corec(T.a:Type × (a ⟶ T))


Proof




Definitions occuring in Statement :  coSet: coSet{i:l} corec: corec(T.F[T]) subtype_rel: A ⊆B function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  and: P ∧ Q ext-eq: A ≡ B coSet: coSet{i:l} so_apply: x[s] so_lambda: λ2x.t[x] member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  coW-corec
Rules used in proof :  productElimination hypothesis hypothesisEquality lambdaEquality sqequalRule universeEquality thin isectElimination sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution sqequalHypSubstitution extract_by_obid introduction cut

Latex:
coSet\{i:l\}  \msubseteq{}r  corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))



Date html generated: 2018_07_29-AM-09_49_27
Last ObjectModification: 2018_07_21-PM-07_14_03

Theory : constructive!set!theory


Home Index