Nuprl Lemma : ml-revappend_wf

[T:Type]. ∀[as,bs:T List].  (ml-revappend(as;bs) ∈ List) supposing valueall-type(T)


Proof




Definitions occuring in Statement :  ml-revappend: ml-revappend(as;bs) list: List valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a
Lemmas referenced :  ml-revappend-sq rev-append_wf list_wf valueall-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis cumulativity axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].    (ml-revappend(as;bs)  \mmember{}  T  List)  supposing  valueall-type(T)



Date html generated: 2017_09_29-PM-05_51_08
Last ObjectModification: 2017_05_10-PM-06_30_09

Theory : ML


Home Index