+++ /dev/null
-alias nat /Coq/Init/Datatypes/nat.ind#1/1
-alias eq /Coq/Init/Logic/eq.ind#1/1
-alias eq_ind /Coq/Init/Logic/eq_ind.con
-alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1
-alias O /Coq/Init/Datatypes/nat.ind#1/1/1
-alias S /Coq/Init/Datatypes/nat.ind#1/1/2
-alias plus /Coq/Init/Peano/plus.con
-alias mult /Coq/Init/Peano/mult.con
-alias le /Coq/Init/Peano/le.ind#1/1
-alias lt /Coq/Init/Peano/lt.con
-alias not /Coq/Init/Logic/not.con
-alias and /Coq/Init/Logic/and.ind#1/1
-alias prod /Coq/Init/Datatypes/prod.ind#1/1
-alias list /Coq/Lists/PolyList/list.ind#1/1
-alias AllS_assoc /Coq/Lists/TheoryList/AllS_assoc.ind#1/1
-alias V /Coq/Lists/PolyList/Lists/A.var
-alias VA /Coq/Lists/TheoryList/Lists/A.var
-alias VB /Coq/Lists/TheoryList/Lists/Assoc_sec/B.var
-
-!A:Set.!B:Set.!P:!a:A.Prop.!l:list{V := (prod A B)}.
- !H:(AllS_assoc {VA := A ; VB := B} P l).
- (and
- (eq list{V := (prod A B)} l l)
- (eqT !n:A.Prop P P))
-
-(* Intros; Elim H:
-
-?1: (A,B:Set; P:(A->Prop); l:(list A*B))
- (AllS_assoc A B P l) -> (nil A*B)=(nil A*B)/\P==P
-?2: (A,B:Set; P:(A->Prop); l:(list A*B))
- (AllS_assoc A B P l) ->
- (a:A; b:B; l0:(list A*B))
- (P a) -> (AllS_assoc A B P l0) -> l0=l0/\P==P ->
- (cons (a,b) l0)=(cons (a,b) l0)/\P==P
-[A,B:Set; P:(A->Prop); l:(list A*B); H:(AllS_assoc A B P l)]
- (AllS_assoc_ind A B P [l0:(list A*B)]l0=l0/\P==P
- (?1 A B P l H) (?2 A B P l H) l H)
-
-*)