(eq list{V := (prod A B)} l l)
(eqT !n:A.Prop P P))
+\forall A,B: Set. \forall P: A \to Prop.
+ \forall l: list \subst [ A \Assign (prod A B) ].
+ \forall H:(AllS_assoc \subst [ A \Assign A ; B \Assign B] P l).
+ l = l \wedge P = P
+
(* Intros; Elim H:
?1: (A,B:Set; P:(A->Prop); l:(list A*B))