diff options
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 }. |