Nuprl Lemma : ex-sqle_transitivity

[e:Atom2]. ∀[a,b,c:Base].  (ex-sqle(e;a;c)) supposing (ex-sqle(e;b;c) and ex-sqle(e;a;b))


Definitions occuring in Statement :  ex-sqle: ex-sqle(e;t;t') atom: Atom$n uimplies: supposing a uall: [x:A]. B[x] base: Base
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a ex-sqle: ex-sqle(e;t;t') prop: all: x:A. B[x] subtype_rel: A ⊆B implies:  Q
Lemmas referenced :  ex-sqle_wf base_wf sqle_trans atom2_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution sqequalRule axiomSqleEquality hypothesis extract_by_obid isectElimination thin hypothesisEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry atomnEquality dependent_functionElimination baseApply closedConclusion baseClosed applyEquality independent_functionElimination

\mforall{}[e:Atom2].  \mforall{}[a,b,c:Base].    (ex-sqle(e;a;c))  supposing  (ex-sqle(e;b;c)  and  ex-sqle(e;a;b))

Date html generated: 2017_02_20-AM-10_46_43
Last ObjectModification: 2017_01_25-PM-05_03_23

Theory : call!by!value_1

Home Index