Nuprl Lemma : decide-exception-type

[T:Type]. ∀[x:T]. ∀[A,B:Top].  case of inl(u) => A[u] inr(v) => B[v] supposing exception-type(T)


Definitions occuring in Statement :  exception-type: exception-type(T) uimplies: supposing a uall: [x:A]. B[x] top: Top so_apply: x[s] decide: case of inl(x) => s[x] inr(y) => t[y] universe: Type sqequal: t
Definitions unfolded in proof :  uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] exception-type: exception-type(T) squash: T iff: ⇐⇒ Q and: P ∧ Q implies:  Q rev_implies:  Q
Lemmas referenced :  exception-type_wf top_wf
Rules used in proof :  universeEquality equalitySymmetry equalityTransitivity because_Cache isect_memberEquality sqequalRule hypothesisEquality thin isectElimination sqequalHypSubstitution lemma_by_obid axiomSqEquality hypothesis pointwiseFunctionality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_isectElimination closedConclusion baseApply baseClosed imageMemberEquality imageElimination exceptionSqequal axiomEquality sqequalExtensionalEquality independent_pairFormation Error :lambdaFormation_alt,  Error :universeIsType,  sqequalIntensionalEquality

\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[A,B:Top].
    case  x  of  inl(u)  =>  A[u]  |  inr(v)  =>  B[v]  \msim{}  x  supposing  exception-type(T)

Date html generated: 2019_06_20-AM-11_20_53
Last ObjectModification: 2018_10_15-PM-03_25_59

Theory : call!by!value_1

Home Index