Nuprl Lemma : inl_equal

[A,B:Type]. ∀[x,y:A].  uiff((inl x) (inl y) ∈ (A B);x y ∈ A)


Proof




Definitions occuring in Statement :  uiff: uiff(P;Q) uall: [x:A]. B[x] inl: inl x union: left right universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a outl: outl(x) prop: isl: isl(x) assert: b ifthenelse: if then else fi  btrue: tt true: True
Lemmas referenced :  and_wf equal_wf outl_wf assert_wf isl_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation sqequalRule hypothesisEquality equalitySymmetry dependent_set_memberEquality hypothesis equalityTransitivity extract_by_obid sqequalHypSubstitution isectElimination thin unionEquality applyEquality lambdaEquality setElimination rename productElimination independent_isectElimination promote_hyp hyp_replacement Error :applyLambdaEquality,  natural_numberEquality setEquality cumulativity inlEquality independent_pairEquality isect_memberEquality axiomEquality because_Cache universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[x,y:A].    uiff((inl  x)  =  (inl  y);x  =  y)



Date html generated: 2016_10_25-AM-10_50_45
Last ObjectModification: 2016_07_12-AM-06_59_36

Theory : general


Home Index