1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
Module Type TITI.
Parameter B:Set.
Parameter x:B.
Inductive A:Set:=
a1:B->A.
Definition f2: A ->B
:= fun (a:A) =>
match a with
(a1 b)=>b
end.
Definition f: A -> B:=fun (a:A) => x.
End TITI.
Module Type TIT.
Declare Module t:TITI.
End TIT.
Module Seq(titi:TIT).
Module t:=titi.t.
Inductive toto:t.A->t.B->Set:=
t1:forall (a:t.A), (toto a (t.f a))
| t2:forall (a:t.A), (toto a (t.f2 a)).
End Seq.
Module koko(tit:TIT).
Module seq:=Seq tit.
Module t':=tit.t.
Definition def:forall (a:t'.A), (seq.toto a (t'.f a)).
intro ; constructor 1.
Defined.
Definition def2: forall (a:t'.A), (seq.toto a (t'.f2 a)).
intro; constructor 2.
(* Toplevel input, characters 0-13
constructor 2.
^^^^^^^^^^^^^
Error: Impossible to unify (seq.toto ?3 (seq.t.f2 ?3)) with
(seq.toto a (t'.f2 a)).*)
Abort.
End koko.
|
