Checking whether or not a logical sequence that ha

Question

Alright I'm writing a program to read a bunch of text files containing logical sequences such as:

[and(p,q), and(r,s)].

and(p,s).

[
  [1, and(p,q),  premise],
  [2, and(r,s),  premise],
  [3, p,         andel1(1)],
  [4, s,         andel2(2)],
  [5, and(p,s),  andint(3,4)]
].

And then check if the proof is valid or not. So far so good, I've written all predicates I can think of for rules that don't include assumptions, and it works. Here is the code so far:

verify(InputFileName) :- see(InputFileName),
                         read(Prems), read(Goal), read(Proof),
                         seen,
                         valid_proof(Prems, Goal, Proof).


valid_proof(_Prems, _Goal, Proof) :-
    valid_proof_(Proof, Proof).

valid_proof_(_, []).
valid_proof_(Proof, [Line|Lines]) :-
    valid_line(Proof, Line),
    valid_proof_(Proof, Lines).

valid_line(_Proof, [_N, _S, premise]).

valid_line(Proof, [_Ln3, U, impel(Ln2, Ln1)]) :-
    member([Ln1, imp(O, U), _], Proof),
    member([Ln2, O, _], Proof).

valid_line(Proof, [_, and(A,B), andint(Ln,Lm)]) :-
    member([Ln, A, _], Proof),
    member([Lm, B, _], Proof).

valid_line(Proof, [_, A, andel1(N)]) :-
    member([N, and(A,_B), _], Proof).

valid_line(Proof, [_, B, andel2(N)]) :-
    member([N, and(_A,B), _], Proof).

valid_line(Proof, [_, or(A,_B), orint1(N)]) :-
    member([N, A, _], Proof).

valid_line(Proof, [_, or(_A,B), orint2(N)]) :-
    member([N, B, _], Proof).

valid_line(Proof, [_, A, copy(N)]) :-
    member([N, A, _], Proof).

valid_line(Proof, [_, neg(O), mt(N1, N2)]) :-
    member([N1, imp(O,U), _], Proof),
    member([N2, neg(U), _], Proof).

valid_line(Proof, [_, O, negnegel(N)]) :-
    member([N, neg(neg(O)), _], Proof).

valid_line(Proof, [_, neg(neg(O)), negnegint(N)]) :-
    member([N, O, _], Proof).

valid_line(Proof, [_, or(O, neg(O)), lem]) :-
    member([_, _, _], Proof).

Problem is that I now have to solve the problem to do the same thing to proofs using assumptions, for instance:

[q].
imp(p,q).
[
    [1, q,        premise],
    [
      [2, p,      assumption],
      [3, q,      copy(1)]
    ],
    [4, imp(p,q), impint(2,3)]
].

I can't do it using the same pattern I've used with the others because now it's lists within a list. So something like this:

valid_line(Proof, [_, imp(O, U), impint(N1, N2)]) :-
    member([N1, O, assumption], Proof),
    member([N2, U, _], Proof),
    N1 < N2.

Wouldn't work. So I'm a bit stuck, I don't know how to proceed.