Nuprl - Proof: filter append sq

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: filter append sq

T:Type, P:(T

), A:T List, B:Top.

filter(P;A @ B) ~ (filter(P;A) @ filter(P;B))

By:	InductionOnList THEN Reduce 0 THEN Try (Complete Auto) THEN SplitOnConclITE THEN Try Trivial THEN Reduce 0 THEN Analyze 0 THEN Analyze THEN Try Trivial THEN BackThruSomeHyp

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html