diff options
| author | filliatr | 2003-12-16 15:54:06 +0000 |
|---|---|---|
| committer | filliatr | 2003-12-16 15:54:06 +0000 |
| commit | 22a24e1cadd4e1206db195c9ef19ca3130eb1bc8 (patch) | |
| tree | b679e3a64f57c8738388d08cc6627cc7a518f23a /doc/Program.tex | |
| parent | d418004b79b5f95898eafa0b5376d5afc30cd699 (diff) | |
tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8401 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Program.tex')
| -rw-r--r-- | doc/Program.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Program.tex b/doc/Program.tex index ddcf8d920f..aa900ecb90 100644 --- a/doc/Program.tex +++ b/doc/Program.tex @@ -607,7 +607,7 @@ Lemma permut_app_app : (m1,m2,n1,n2 :list) (permut m1 n1)->(permut m2 n2)->(permut (app m1 m2) (app n1 n2)). Intros m1 m2 n1 n2 h1 h2. Elim h1 ; Intros. - Exact h2. + exact h2. Apply permut_tran with (app m n2) ; Auto. Apply permut_tran with (app m m2) ; Auto. Auto. @@ -692,7 +692,7 @@ Inductive sort : list->Prop := Hints Resolve sort_nil sort_mil. Lemma permutapp : (a0:A)(y,l1,l2:list)(permut y (app l1 l2))->(permut (cons a0 y) (app l1 (cons a0 l2))). Intros. -Exact (permut_cmil a0 y l1 l2 H). +exact (permut_cmil a0 y l1 l2 H). Save. Hints Resolve permutapp. Lemma sortmil : (a:A)(x,x0,l1,l2:list)(sup_list a l1)->(inf_list a l2)->(sort x)->(sort x0)->(permut l1 x)->(permut l2 x0)->(sort (mil a x x0)). |