Nuprl Lemma : safety_wf

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


Proof




Definitions occuring in Statement :  safety: safety(A;tr.P[tr]) list: List uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T safety: safety(A;tr.P[tr]) so_lambda: λ2x.t[x] implies:  Q prop: so_apply: x[s]
Lemmas referenced :  all_wf list_wf iseg_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality functionEquality applyEquality axiomEquality equalityTransitivity equalitySymmetry functionIsType universeIsType universeEquality isect_memberEquality cumulativity

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



Date html generated: 2019_10_15-AM-10_54_03
Last ObjectModification: 2018_09_27-AM-09_37_33

Theory : list!


Home Index