diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /theories | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/StrictProp.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Logic/StrictProp.v b/theories/Logic/StrictProp.v index af97b60ee6..b12867ad4e 100644 --- a/theories/Logic/StrictProp.v +++ b/theories/Logic/StrictProp.v @@ -23,9 +23,6 @@ Arguments squash {_} _. Inductive sEmpty : SProp :=. Inductive sUnit : SProp := stt. -Definition sUnit_rect (P:sUnit -> Type) (v:P stt) (u:sUnit) : P u := v. -Definition sUnit_rec (P:sUnit -> Set) (v:P stt) (u:sUnit) : P u := v. -Definition sUnit_ind (P:sUnit -> Prop) (v:P stt) (u:sUnit) : P u := v. Set Primitive Projections. Record Ssig {A:Type} (P:A->SProp) := Sexists { Spr1 : A; Spr2 : P Spr1 }. |