blob: c348626921f498a37a7ea662294057ed5aa3700f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Axiom IsTrunc : Type -> Type.
Existing Class IsTrunc.
Declare Instance trunc_forall :
forall (A : Type) (P : A -> Type),
IsTrunc (forall a : A, P a).
Axiom Graph : Set.
Axiom in_N : forall (n : Graph), Type.
Definition N : Type := @sigT Graph in_N.
Goal forall (P : N -> Type)
(Q := fun m : Graph => forall mrec : in_N m, P (existT _ m mrec))
(A : Graph), IsTrunc (Q A).
Proof.
intros.
solve [typeclasses eauto].
Qed.
|
