1 alias nat /Coq/Init/Datatypes/nat.ind#1/1
2 alias eq /Coq/Init/Logic/Equality/eq.ind#1/1
3 alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con
4 alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1
5 alias O /Coq/Init/Datatypes/nat.ind#1/1/1
6 alias S /Coq/Init/Datatypes/nat.ind#1/1/2
7 alias plus /Coq/Init/Peano/plus.con
8 alias mult /Coq/Init/Peano/mult.con
9 alias le /Coq/Init/Peano/le.ind#1/1
10 alias lt /Coq/Init/Peano/lt.con
11 alias not /Coq/Init/Logic/not.con
12 alias and /Coq/Init/Logic/Conjunction/and.ind#1/1
13 alias prod /Coq/Init/Datatypes/prod.ind#1/1
14 alias list /Coq/Lists/PolyList/Lists/list.ind#1/1
15 alias AllS_assoc /Coq/Lists/TheoryList/Lists/Assoc_sec/AllS_assoc.ind#1/1
17 !A:Set.!B:Set.!P:!a:A.Prop.!l:(list (prod A B)).
18 !H:(AllS_assoc A B P l).
20 (eq (list (prod A B)) l l)
25 ?1: (A,B:Set; P:(A->Prop); l:(list A*B))
26 (AllS_assoc A B P l) -> (nil A*B)=(nil A*B)/\P==P
27 ?2: (A,B:Set; P:(A->Prop); l:(list A*B))
28 (AllS_assoc A B P l) ->
29 (a:A; b:B; l0:(list A*B))
30 (P a) -> (AllS_assoc A B P l0) -> l0=l0/\P==P ->
31 (cons (a,b) l0)=(cons (a,b) l0)/\P==P
32 [A,B:Set; P:(A->Prop); l:(list A*B); H:(AllS_assoc A B P l)]
33 (AllS_assoc_ind A B P [l0:(list A*B)]l0=l0/\P==P
34 (?1 A B P l H) (?2 A B P l H) l H)