match ps with
| []   => intro; exact h
| [p]  => unfold andN
          unfold impliesN at h
          exact h
| p₁::p₂::ps => unfold andN
                unfold impliesN at h
                intro ⟨hp₁, hps⟩
                revert hps
                exact scopes (h hp₁)
ps : List Prop
q : Prop
h : impliesN ps q
⊢ andN ps → q
no goals