Nuprl Lemma : safety_and

[A:Type]. ∀[P,Q:(A List) ⟶ ℙ].  (safety(A;x.P[x])  safety(A;x.Q[x])  safety(A;x.P[x] ∧ Q[x]))


Proof




Definitions occuring in Statement :  safety: safety(A;tr.P[tr]) list: List uall: [x:A]. B[x] prop: so_apply: x[s] implies:  Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  safety: safety(A;tr.P[tr]) uall: [x:A]. B[x] implies:  Q all: x:A. B[x] and: P ∧ Q cand: c∧ B member: t ∈ T prop: so_apply: x[s] subtype_rel: A ⊆B so_lambda: λ2x.t[x] guard: {T}
Lemmas referenced :  subtype_rel_self iseg_wf list_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt lambdaFormation sqequalHypSubstitution productElimination thin cut independent_pairFormation hypothesis productEquality applyEquality hypothesisEquality instantiate introduction extract_by_obid isectElimination universeEquality because_Cache lambdaEquality functionEquality inhabitedIsType functionIsType universeIsType dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[A:Type].  \mforall{}[P,Q:(A  List)  {}\mrightarrow{}  \mBbbP{}].    (safety(A;x.P[x])  {}\mRightarrow{}  safety(A;x.Q[x])  {}\mRightarrow{}  safety(A;x.P[x]  \mwedge{}  Q[x]))



Date html generated: 2019_10_15-AM-10_54_10
Last ObjectModification: 2018_09_27-AM-10_02_41

Theory : list!


Home Index