-------------                        
                          s(b,[b],[])       p([],[])        ∀E,L,R,P. s(E,L,R) ∧ p(R,P) → p(L,[E|P])
                        -----------------------------      -------------------------------------------- (∀-E)
                         (s(b,[b],[]) ∧ p([],[]) )          s(b,[b],[]) ∧ p([],[]) → p([b],[b|[]])
   --------------       ----------------------------------------------------------------------------- (MP)
   s(a,[a,b],[b])                          p([b],[b|[]])                                                                               (2)
  --------------------------------------------------------                                                       ------------------------------------------------------ (∀-E)
                s(a,[a,b],[b]) ∧ p([b],[b|[]])                                                                    s(a,[a,b],[b]) ∧ p([b],[b|[]]) → p([a,b],[a|[b|[]]])
              --------------------------------------------------------------------------------------------------------------------------------------------------------- (MP)
                                                                           p([a,b],[a|[b|[]]])
                                                                         ---------------------- (∃-I)
                                                                             ∃P. p([a,b],P)