From c63e930e342efe4205afb616564abae6350b3e38 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 Oct 2002 14:08:04 +0000 Subject: [PATCH] explicit namd substitutions introduced --- helm/gTopLevel/esempi/elim2.cic | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/helm/gTopLevel/esempi/elim2.cic b/helm/gTopLevel/esempi/elim2.cic index da7753966..b7c01b96a 100644 --- a/helm/gTopLevel/esempi/elim2.cic +++ b/helm/gTopLevel/esempi/elim2.cic @@ -1,6 +1,6 @@ alias nat /Coq/Init/Datatypes/nat.ind#1/1 -alias eq /Coq/Init/Logic/Equality/eq.ind#1/1 -alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con +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 @@ -9,15 +9,18 @@ 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/Conjunction/and.ind#1/1 +alias and /Coq/Init/Logic/and.ind#1/1 alias prod /Coq/Init/Datatypes/prod.ind#1/1 -alias list /Coq/Lists/PolyList/Lists/list.ind#1/1 -alias AllS_assoc /Coq/Lists/TheoryList/Lists/Assoc_sec/AllS_assoc.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 (prod A B)). - !H:(AllS_assoc A B P l). +!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 (prod A B)) l l) + (eq list{V := (prod A B)} l l) (eqT !n:A.Prop P P)) (* Intros; Elim H: -- 2.39.2