blob: 8a607c936d20ba4b58e16361786884292bcedd3d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Structure Inner := mkI { is :> Type }.
Structure Outer := mkO { os :> Inner }.
Canonical Structure natInner := mkI nat.
Canonical Structure natOuter := mkO natInner.
Definition hidden_nat := nat.
Axiom P : forall S : Outer, is (os S) -> Prop.
Lemma foo (n : hidden_nat) : P _ n.
Admitted.
|
