]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/esempi/elim2.cic
snapshot
[helm.git] / helm / gTopLevel / esempi / elim2.cic
1 alias nat        /Coq/Init/Datatypes/nat.ind#1/1
2 alias eq         /Coq/Init/Logic/eq.ind#1/1
3 alias eq_ind     /Coq/Init/Logic/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/and.ind#1/1
13 alias prod       /Coq/Init/Datatypes/prod.ind#1/1 
14 alias list       /Coq/Lists/PolyList/list.ind#1/1
15 alias AllS_assoc /Coq/Lists/TheoryList/AllS_assoc.ind#1/1
16 alias V          /Coq/Lists/PolyList/Lists/A.var
17 alias VA         /Coq/Lists/TheoryList/Lists/A.var
18 alias VB         /Coq/Lists/TheoryList/Lists/Assoc_sec/B.var
19
20 !A:Set.!B:Set.!P:!a:A.Prop.!l:list{V := (prod A B)}.
21  !H:(AllS_assoc {VA := A ; VB := B} P l).
22   (and
23    (eq list{V := (prod A B)} l l)
24    (eqT !n:A.Prop P P))
25
26 \forall A,B: Set. \forall P: A \to Prop.
27  \forall l: list \subst [ A \Assign (prod A B) ].
28   \forall H:(AllS_assoc \subst [ A \Assign A ; B \Assign B] P l).
29     l = l \wedge P = P
30
31 (* Intros; Elim H:
32
33 ?1: (A,B:Set; P:(A->Prop); l:(list A*B))
34      (AllS_assoc A B P l) -> (nil A*B)=(nil A*B)/\P==P
35 ?2: (A,B:Set; P:(A->Prop); l:(list A*B))
36      (AllS_assoc A B P l) ->
37       (a:A; b:B; l0:(list A*B))
38        (P a) -> (AllS_assoc A B P l0) -> l0=l0/\P==P ->
39         (cons (a,b) l0)=(cons (a,b) l0)/\P==P
40 [A,B:Set; P:(A->Prop); l:(list A*B); H:(AllS_assoc A B P l)]
41  (AllS_assoc_ind A B P [l0:(list A*B)]l0=l0/\P==P
42   (?1 A B P l H) (?2 A B P l H) l H)
43
44 *)