IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter append T:Type, P:(T), l1,l2:T List.
filter(P;l1 @ l2) ~ (filter(P;l1) @ filter(P;l2))
By:
ObviousListInduction
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, P:(T
), l1,l2:T List.
filter(P;l1 @ l2) ~ (filter(P;l1) @ filter(P;l2))
