blob: 8774e191c1ad06acb8d9b3944d9469ae1f57c8dd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import ssreflect.
Set Universe Polymorphism.
Cumulative Variant paths {A} (x:A) : A -> Type
:= idpath : paths x x.
Register paths as core.eq.type.
Register idpath as core.eq.refl.
Lemma case_test (b:bool) : paths b b.
Proof. case B:b; reflexivity. Qed.
|
