blob: aa8da53361e322e13920b73931d386bc7247d95d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Set Universe Polymorphism.
Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x.
Inductive unit@{i} : Type@{i} := tt.
Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n.
Proof.
intros m n P e p.
abstract (rewrite e in p; exact p).
Defined.
Check foo_subproof@{Set Set}.
Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n.
Proof.
intros m n P e p.
abstract (rewrite e in p; exact p).
Defined.
Check bar_subproof@{Set Set}.
|
