blob: 9d33fafc4ceb95214967971d10471527ccdd1b28 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Module Type T.
Parameter f : nat -> Type.
End T.
Module F(A:T).
Inductive ind : Prop :=
C : A.f 0 -> ind.
End F.
Module A. Definition f (x:nat) := True. End A.
Module M := F A.
(* M.ind could eliminate into Set/Type even though F.ind can't *)
|
