diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1931.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1931.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v index bc8be78f..930ace1d 100644 --- a/test-suite/bugs/closed/shouldsucceed/1931.v +++ b/test-suite/bugs/closed/shouldsucceed/1931.v @@ -8,7 +8,7 @@ Inductive T (A:Set) : Set := Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B := match t with app t1 t2 => app (map f t1)(map f t2) - end. + end. Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B := match t with @@ -19,7 +19,7 @@ Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B := Definition k0:=Set. (** interaction of subst with map *) -Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): +Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): subst g (map f t) = subst (fun x => g (f x)) t. Proof. intros. |