diff --git a/typed-racket-lib/typed-racket/base-env/base-env.rkt b/typed-racket-lib/typed-racket/base-env/base-env.rkt
index 14e5227b8..0af4e779f 100644
--- a/typed-racket-lib/typed-racket/base-env/base-env.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-env.rkt
@@ -1553,7 +1553,7 @@
 [system-idle-evt (-> (-evt -Void))]
 [alarm-evt (-> -Real (-mu x (-evt x)))]
 [handle-evt? (asym-pred Univ B (-PS (-is-type 0 (-evt Univ)) -tt))]
-[prop:evt (-struct-property (Un (-evt Univ) (-> -Self ManyUniv) -Nat) #'evt?)]
+[prop:evt (-struct-property (Un (-evt Univ) (-> -Self Univ) -Nat) #'evt?)]
 [current-evt-pseudo-random-generator
  (-Param -Pseudo-Random-Generator -Pseudo-Random-Generator)]
 
diff --git a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
index 4dbd7384d..872721247 100644
--- a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
+++ b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
@@ -102,13 +102,15 @@
                                ([val (attribute prop-val)]
                                 [name (attribute prop)])
                        (cond
-                         [(free-identifier=? name #'prop:procedure)
+                         [(or (free-identifier=? name #'prop:procedure)
+                              (free-identifier=? name #'prop:evt))
                           (define tname (or (attribute type) st-name))
                           (define sty-stx (if (null? type-vars)
                                               tname
                                               (quasisyntax/loc tname
                                                 (#,tname #,@type-vars))))
-                          (maybe-extract-prop-proc-ty-ann sty-stx val)]
+                          (define-values (val^ ty^) (extract-prop-specified-type-ann sty-stx val))
+                          (values val^ (assoc-struct-property-name-property ty^ name))]
                          [else (values val #f)])))]
              #:attr proc-ty (if (null? proc-tys) #f
                                 proc-tys)
@@ -199,17 +201,17 @@
                 . opts))]))
 
 
-;; This function tries to extract the type annotation on a lambda
-;; expression for prop:precedure.
+;; This function tries to extract the type annotation from values for
+;; prop:procedure or prop:evt
 ;;
 ;; sty-stx: the syntax that represents a structure type. For a monomorhpic
 ;; structure type, sty-stx is the identifier for its name. For a polymorphic
 ;; structure type, sty-stx is in the form (structure-name type-vars ...)
 ;;
-;; val: the value expression for prop:procedure
+;; val: the value expression for the property
 ;;
 ;;Syntax Expr -> (values Syntax Syntax)
-(define-for-syntax (maybe-extract-prop-proc-ty-ann sty-stx val)
+(define-for-syntax (extract-prop-specified-type-ann sty-stx val)
   (syntax-parse val
     #:literals (-lambda ann)
     [(-lambda formals:lambda-formals ret-ty:return-ann _)
diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt
index 67ae08d39..18730c027 100644
--- a/typed-racket-lib/typed-racket/env/init-envs.rkt
+++ b/typed-racket-lib/typed-racket/env/init-envs.rkt
@@ -265,11 +265,11 @@
      `(make-Name (quote-syntax ,stx) ,args ,struct?)]
     [(fld: t acc mut)
      `(make-fld ,(type->sexp t) (quote-syntax ,acc) ,mut)]
-    [(Struct: name parent flds proc poly? pred-id properties)
+    [(Struct: name parent flds extra-tys poly? pred-id properties)
      `(make-Struct (quote-syntax ,name)
                    ,(and parent (type->sexp parent))
                    (list ,@(map type->sexp flds))
-                   ,(and proc (type->sexp proc))
+                   ,(and extra-tys `(list ,@(map type->sexp extra-tys)))
                    ,poly?
                    (quote-syntax ,pred-id)
                    (immutable-free-id-set (list ,@(for/list ([p (in-free-id-set properties)])
diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index d683e26ab..f0924e492 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -681,14 +681,17 @@
 
         ;; two structs with the same name
         ;; just check pairwise on the fields
-        [((Struct: nm _ flds proc _ _ _) (Struct: nm* _ flds* proc* _ _ _))
+        [((Struct: nm _ flds extra-ty _ _ _) (Struct: nm* _ flds* extra-ty* _ _ _))
          #:when (free-identifier=? nm nm*)
-         (let ([proc-c
-                (cond [(and proc proc*)
-                       (cg proc proc*)]
-                      [proc* #f]
+         (let ([extra-ty-c
+                (cond [(and extra-ty extra-ty*)
+                       (for/fold ([acc empty])
+                                  ([p extra-ty]
+                                   [p* extra-ty*])
+                         (% cset-meet acc (cg p p*)))]
+                      [extra-ty* #f]
                       [else empty])])
-           (% cset-meet proc-c (cgen/flds context flds flds*)))]
+           (% cset-meet extra-ty-c (cgen/flds context flds flds*)))]
 
         ;; two prefab structs with the same key
         [((Prefab: k ss) (Prefab: k* ts))
diff --git a/typed-racket-lib/typed-racket/private/syntax-properties.rkt b/typed-racket-lib/typed-racket/private/syntax-properties.rkt
index ff753e9a6..4f7a3c470 100644
--- a/typed-racket-lib/typed-racket/private/syntax-properties.rkt
+++ b/typed-racket-lib/typed-racket/private/syntax-properties.rkt
@@ -61,6 +61,7 @@
   (type-inst type-inst)
   (row-inst row-inst)
   (st-proc-ty st-proc-ty)
+  (assoc-struct-property-name assoc-struct-property-name)
   (type-label type-label)
   (optional-non-immediate-arg optional-non-immediate-arg)
   (optional-immediate-arg optional-immediate-arg)
diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt
index 757cd77f4..191f12395 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -727,10 +727,10 @@
                               " with unknown return values"))]
           [(Values: (list (Result: rngs _ _) ...))
            (unit/sc imports-specs exports-specs init-depends-ids (map t->sc rngs))])]
-       [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred? props)
+       [(Struct: nm par (list (fld: flds acc-ids mut?) ...) extra-tys poly? pred? props)
         (cond
           [(hash-ref recursive-values nm #f)]
-          [proc (fail #:reason "procedural structs are not supported")]
+          [extra-tys (fail #:reason "structs with prop:procedure or prop:evt attached are not supported")]
           [poly?
            (struct->recursive-sc #'n* nm flds
                                            (lambda (ftsc)
diff --git a/typed-racket-lib/typed-racket/rep/type-mask.rkt b/typed-racket-lib/typed-racket/rep/type-mask.rkt
index 348797657..4d14f2904 100644
--- a/typed-racket-lib/typed-racket/rep/type-mask.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-mask.rkt
@@ -144,6 +144,7 @@
  mask:other-box
  mask:set
  mask:procedure
+ mask:evt
  mask:prompt-tag
  mask:continuation-mark-key
  mask:struct
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 094a4b5cf..eb632a15e 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -76,7 +76,7 @@
                      [Struct:* Struct:]
                      [Row* make-Row]
                      [make-Mu unsafe-make-Mu]
-                     [Struct-proc* Struct-proc]
+                     [Struct-extra-tys* Struct-extra-tys]
                      [make-Struct* make-Struct]
                      [Mu-names: Mu-maybe-name:]
                      [Mu-body Mu-body-unsafe]
@@ -368,7 +368,8 @@
 ;; Evt
 ;;------
 
-(def-structural Evt ([result #:covariant]))
+(def-structural Evt ([result #:covariant])
+  [#:mask mask:evt])
 
 ;;--------
 ;; Param
@@ -776,38 +777,42 @@
                   ;; we can only put a function type of this box when checking the property value
                   ;; for prop:procedure, which happens after a Struct rep
                   ;; instance is created.
-                  [proc (box/c (or/c #f Fun?))]
+                  [extra-tys (box/c (or/c #f (listof Type?)))]
                   [poly? boolean?]
                   [pred-id identifier?]
                   [properties (free-id-set/c identifier?)])
-  #:no-provide (Struct: Struct-proc make-Struct)
-  [#:frees (f) (combine-frees (map f (append (let ([bv (unbox proc)])
-                                               (if bv (list bv) null))
+  #:no-provide (Struct: Struct-extra-tys make-Struct)
+  [#:frees (f) (combine-frees (map f (append (let ([bv (unbox extra-tys)])
+                                               (if bv bv null))
                                              (if parent (list parent) null)
                                              flds)))]
   [#:fmap (f) (make-Struct name
                            (and parent (f parent))
                            (map f flds)
-                           (let ([bv (unbox proc)])
-                             (box (and bv (f bv))))
+                           (let ([bv (unbox extra-tys)])
+                             (box (and bv (map f bv))))
                            poly?
                            pred-id
                            properties)]
   [#:for-each (f)
    (when parent (f parent))
    (for-each f flds)
-   (when proc (f proc))]
+   (let ([bv (unbox extra-tys)])
+     (when bv (for-each f bv)))]
   ;; This should eventually be based on understanding of struct properties.
-  [#:mask (mask-union mask:struct mask:procedure)]
+  [#:mask (mask-union mask:struct mask:procedure mask:evt)]
   [#:custom-constructor
    (let ([name (normalize-id name)]
          [pred-id (normalize-id pred-id)])
-     (make-Struct name parent flds proc poly? pred-id properties))])
+     (make-Struct name parent flds extra-tys poly? pred-id properties))])
 
 
-(define/cond-contract (Struct-proc* sty)
-  (-> Struct? (or/c #f Fun?))
-  (define b (Struct-proc sty))
+(define/cond-contract (Struct-extra-tys* sty)
+  (-> (or/c Poly? Struct?) (or/c #f (listof Type?)))
+  (define sty^ (match sty
+                 [(? Struct?) sty]
+                 [(Poly: _ (? Struct? sty)) sty]))
+  (define b (Struct-extra-tys sty^))
   (and b (unbox b)))
 
 (define (make-Struct* name parent flds proc poly? pred-id properties)
@@ -816,8 +821,8 @@
 (define-match-expander Struct:*
   (lambda (stx)
     (syntax-case stx ()
-      [(_ name parent flds proc poly? pred-id properties)
-       #'(Struct: name parent flds (box proc) poly? pred-id properties)])))
+      [(_ name parent flds extra-tys poly? pred-id properties)
+       #'(Struct: name parent flds (box extra-tys) poly? pred-id properties)])))
 
 
 (def-type StructTop ([name Struct?])
@@ -826,6 +831,10 @@
   [#:for-each (f) (f name)]
   [#:mask (mask-union mask:struct mask:procedure)])
 
+(def-type Undecided-Evt ([n F?])
+  [#:frees (f) (f n)]
+  [#:fmap (f) (make-Undecide)])
+
 ;; Represents prefab structs
 ;; key  : prefab key encoding mutability, auto-fields, etc.
 ;; flds : the types of all of the prefab fields
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 22fa3cb3a..ee439a762 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -91,13 +91,6 @@
   (syntax-parse stx
     [t:typed-struct #'t.type-name]))
 
-;; a simple wrapper to get proc from a polymorphic or monomorhpic structure
-(define/cond-contract (get-struct-proc sty)
-  (c:-> (c:or/c Struct? Poly?) (c:or/c #f Fun?))
-  (Struct-proc (match sty
-                 [(? Struct?) sty]
-                 [(Poly: names (? Struct? sty)) sty])))
-
 
 (define/cond-contract (tc/struct-prop-values st-tname pnames pvals)
   (c:-> identifier? (c:listof identifier?) (c:listof syntax?) void?)
@@ -195,7 +188,7 @@
 ;; Constructs the Struct value for a structure type
 ;; The returned value has free type variables
 (define/cond-contract (mk/inner-struct-type names desc parent [property-names empty] [proc-ty #f])
-  (c:->* (struct-names? struct-desc? (c:or/c Struct? #f)) ((c:listof identifier?) (c:or/c Type? #f)) Struct?)
+  (c:->* (struct-names? struct-desc? (c:or/c Struct? #f)) ((c:listof identifier?) (c:or/c (c:listof Type?) #f)) Struct?)
 
   (let* ([this-flds (for/list ([t (in-list (struct-desc-self-fields desc))]
                                [g (in-list (struct-names-getters names))])
@@ -204,7 +197,7 @@
     (make-Struct (struct-names-struct-name names)
                  parent
                  flds
-                 (or proc-ty (and parent (Struct-proc parent)))
+                 (or proc-ty (and parent (Struct-extra-tys parent)))
                  (not (null? (struct-desc-tvars desc)))
                  (struct-names-predicate names)
                  (immutable-free-id-set property-names))))
@@ -384,9 +377,10 @@
   ;; the alias, with free type variables
   (define st-type-alias (mk-type-alias type-name tvars))
   (define st-type-alias-maybe-with-proc
-    (let ([maybe-proc-ty (and (or (Poly? sty) (Struct? sty))
-                              (get-struct-proc sty))])
-      (if maybe-proc-ty (intersect st-type-alias maybe-proc-ty)
+    (let ([maybe-proc-tys (and (or (Poly? sty) (Struct? sty))
+                              (Struct-extra-tys sty))])
+      (if maybe-proc-tys
+          (foldl intersect st-type-alias maybe-proc-tys)
           st-type-alias)) )
 
   ;; simple abstraction for handling field getters or setters
@@ -463,84 +457,141 @@
       (struct-names-type-name (parsed-struct-names parsed-struct))))
   (refine-variance! names stys tvarss))
 
+
+(define ((make-extract specified-field-checker supplied-proc-checker failure-msg)
+         ty-stx st-name fld-names desc)
+  (syntax-parse ty-stx
+    #:literals (struct-field-index)
+    ;; a field index is provided
+    [n_:exact-nonnegative-integer
+     (define n (syntax-e #'n_))
+     (define max-idx (sub1 (length (struct-desc-self-fields desc))))
+     (unless (<= n max-idx)
+       (tc-error/fields
+        "index too large"
+        "index"
+        n
+        "maximum allowed index"
+        max-idx
+        #:stx ty-stx))
+     (define ty (list-ref (struct-desc-self-fields desc) n))
+     (specified-field-checker ty-stx (list-ref fld-names n) ty)]
+
+    ;; a field name is provided via `struct-field-index`
+    [(struct-field-index fld-nm:id)
+     (define idx (index-of fld-names #'fld-nm free-identifier=?))
+     ;; fld-nm must be valid, because invalid field names have been reported by
+     ;; struct-field-index at this point
+     (specified-field-checker ty-stx #'fld-nm (list-ref (struct-desc-self-fields desc) idx))]
+
+    [ty-stx:st-proc-ty^
+     #:do [(define ty (parse-type #'ty-stx))]
+     (define tvars (struct-desc-tvars desc))
+     (supplied-proc-checker #'ty-stx ty (mk-type-alias st-name tvars))]
+    [_ (tc-error/stx ty-stx failure-msg)]))
+
+(define (mk-handling-entry
+          #:name name
+          #:specified-field-checker specified-field-checker
+          #:supplied-proc-checker suppiled-proc-checker
+          #:failure-msg failure-msg)
+  (cons name (make-extract specified-field-checker suppiled-proc-checker failure-msg)))
+
+(define property-handling-table
+  (make-immutable-free-id-table
+   (list
+    (mk-handling-entry
+      #:name
+      #'prop:procedure
+      #:specified-field-checker
+      (lambda (ty-stx fld-name ty)
+        (unless (Fun? ty)
+          (tc-error/fields
+           (format "field ~a is not a function" (syntax-e fld-name))
+           "expected"
+           "Procedure"
+           "given"
+           ty
+           #:stx ty-stx))
+        ty)
+      #:supplied-proc-checker
+      (lambda (ty-stx ty st-alias)
+        (match ty
+          [(Fun: (list arrs ...))
+           (make-Fun
+            (map (lambda (arr)
+                   (Arrow-update
+                    arr
+                    dom
+                    (lambda (doms)
+                      (match* ((car doms) st-alias)
+                        [((Name/simple: n) (Name/simple: st))
+                         #:when (free-identifier=? n st)
+                         (void)]
+                        [((App: (Name/simple: rator) _) (App: (Name/simple: st) _))
+                         #:when (free-identifier=? rator st)
+                         (void)]
+                        [((Univ:) _)
+                         (void)]
+                        [((or (Name/simple: (app syntax-e n)) n) _)
+                         (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
+                                          "expected" st-alias
+                                          "got" n
+                                          #:stx (st-proc-ty-property ty-stx))])
+                      (cdr doms))))
+                 arrs))]
+          [_
+           (tc-error/fields "type mismatch"
+                            "expected"
+                            "Procedure"
+                            "given"
+                            ty
+                            #:stx ty-stx)]))
+      #:failure-msg
+      "expected: a nonnegative integer literal or an annotated lambda")
+    (mk-handling-entry
+      #:name
+      #'prop:evt
+      #:specified-field-checker
+      (lambda (ty-stx field-name ty)
+        (if (subtype ty (-evt Univ))
+            ty
+            ;; if the field is not an event, we get the "never ready" event type.
+            (make-Evt (Un))))
+      #:supplied-proc-checker
+      (lambda (ty-stx ty st-alias)
+        (match ty
+          [(Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng-t _ _))))))
+           (unless (= (length doms) 1)
+             (tc-error/stx ty-stx
+                           "expected: a function that takes only one argument"))
+           (cond
+             [(subtype rng-t (-evt Univ))
+              rng-t]
+             [(F? rng-t) (make-Evt rng-t)]
+             [else
+              ;; if the return type is not an event, we make an event type using the structure type
+              (make-Evt st-alias)])]
+          [_ (if (subtype ty (-evt Univ))
+                 ty
+                 (tc-error/stx ty-stx
+                               "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))]))
+      #:failure-msg
+      "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))))
+
+
+
 ;; extract the type annotation of prop:procedure value
-(define/cond-contract (extract-proc-ty proc-ty-stx desc fld-names st-name)
-  (c:-> (c:listof syntax?) struct-desc? (c:listof identifier?) identifier? Type?)
+(define/cond-contract (extract-prop-specified-type proc-ty-stx-li desc fld-names st-name)
+  (c:-> (c:listof syntax?) struct-desc? (c:listof identifier?) identifier? (c:listof Type?))
+
 
-  (unless (equal? (length proc-ty-stx) 1)
+  (unless (equal? (length proc-ty-stx-li) 1)
     (tc-error "prop:procedure can only have one value assigned to it"))
 
-  (let ([proc-ty-stx (car proc-ty-stx)])
-    (syntax-parse proc-ty-stx
-      #:literals (struct-field-index)
-      ;; a field index is provided
-      [n_:exact-nonnegative-integer
-       (define n (syntax-e #'n_))
-       (define max-idx (sub1 (length (struct-desc-self-fields desc))))
-       (unless (<= n max-idx)
-         (tc-error/fields
-          "index too large"
-          "index"
-          n
-          "maximum allowed index"
-          max-idx
-          #:stx proc-ty-stx))
-       (define ty (list-ref (struct-desc-self-fields desc) n))
-       (unless (Fun? ty)
-         (tc-error/fields
-          (format "field ~a is not a function" (syntax-e (list-ref fld-names n)))
-          "expected"
-          "Procedure"
-          "given"
-          ty
-          #:stx proc-ty-stx))
-       ty]
-
-      ;; a field name is provided (via struct-field-index)
-      [(struct-field-index fld-nm:id)
-       (define idx (index-of fld-names #'fld-nm
-                             free-identifier=?))
-       ;; fld-nm must be valid, because invalid field names have been reported by
-       ;; struct-field-index at this point
-       (list-ref (struct-desc-self-fields desc) idx)]
-
-      [ty-stx:st-proc-ty^
-       #:do [(define ty (parse-type #'ty-stx))]
-       (match ty
-         [(Fun: (list arrs ...))
-          (make-Fun
-           (map (lambda (arr)
-                  (Arrow-update
-                   arr
-                   dom
-                   (lambda (doms)
-                     (match (car doms)
-                       [(Name/simple: n)
-                        #:when (free-identifier=? n st-name)
-                        (void)]
-                       [(App: (Name/simple: rator) vars)
-                        #:when (free-identifier=? rator st-name)
-                        (void)]
-                       [(Univ:)
-                        (void)]
-                       [(or (Name/simple: (app syntax-e n)) n)
-                        (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
-                                         "expected" (syntax-e st-name)
-                                         "got" n
-                                         #:stx (st-proc-ty-property #'ty-stx))])
-
-                     (cdr doms))))
-                arrs))]
-         [_
-          (tc-error/fields "type mismatch"
-                           "expected"
-                           "Procedure"
-                           "given"
-                           ty
-                           #:stx #'ty-stx)])]
-      [_
-       (tc-error/stx proc-ty-stx
-                     "expected: a nonnegative integer literal or an annotated lambda")])))
+  (for/list ([proc-ty-stx (in-list proc-ty-stx-li)])
+    (define property-name (assoc-struct-property-name-property proc-ty-stx))
+    ((free-id-table-ref property-handling-table property-name) proc-ty-stx st-name fld-names desc)))
 
 ;; check and register types for a define struct
 ;; tc/struct : Listof[identifier] (U identifier (list identifier identifier))
@@ -632,7 +683,7 @@
                                            (and proc-ty-stx
                                                 (not (null? proc-ty-stx))
                                                 (extend-tvars tvars
-                                                              (extract-proc-ty proc-ty-stx desc fld-names type-name)))))
+                                                              (extract-prop-specified-type proc-ty-stx desc fld-names type-name)))))
 
          (parsed-struct sty names desc (struct-info-property nm/par) type-only)]))
 
diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt
index bb2d92470..a73113282 100644
--- a/typed-racket-lib/typed-racket/types/abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/abbrev.rkt
@@ -195,7 +195,12 @@
 
 ;; Structs
 (define (-struct name parent flds [proc #f] [poly #f] [pred #'dummy] [props (immutable-free-id-set)])
-  (make-Struct name parent flds proc poly pred props))
+  (make-Struct name parent flds
+               (cond
+                 [(and proc (not (list? proc)))
+                  (list proc)]
+                 [else proc])
+               poly pred props))
 
 ;; Function type constructors
 (define/decl top-func (make-Fun (list)))
diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt
index dd724196c..2b7ab5706 100644
--- a/typed-racket-lib/typed-racket/types/overlap.rkt
+++ b/typed-racket-lib/typed-racket/types/overlap.rkt
@@ -50,6 +50,13 @@
   (match*/no-order
    (t1 t2)
    [(_ _) #:when (equal? t1 t2) #t]
+   ;; a struct type can overlap with a function type (via prop:procedure)
+   ;; or any event type (via prop:evt)
+   [((or (? Fun?) (? (lambda (x) (subtype x (make-Evt Univ)))))
+     (or (Name/struct: _)
+         (? Struct?)))
+    #:no-order
+    #t]
    [(_ _) #:when (disjoint-masks? (mask t1) (mask t2)) #f]
    [(_ _) #:when (seen? t1 t2) #t]
    [((Univ:) _) #:no-order #t]
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 6342c2d8b..7525b0dd1 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -660,10 +660,10 @@
     [(? improper-tuple? t)
      `(List* ,@(map type->sexp (improper-tuple-elems t)))]
     [(Opaque: pred) `(Opaque ,(syntax->datum pred))]
-    [(Struct: nm par (list (fld: t _ _) ...) proc _ _ properties)
+    [(Struct: nm par (list (fld: t _ _) ...) extra-tys _ _ properties)
      `#(,(string->symbol (format "struct:~a" (syntax-e nm)))
         ,(map t->s t)
-        ,@(if proc (list (t->s proc)) null)
+        ,@(if extra-tys (list (map t->s extra-tys)) null)
         ,@(free-id-set->list properties))]
     [(? Fun?)
      (parameterize ([current-print-type-fuel
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index 652a1f5a6..dc8126d0d 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -1205,7 +1205,7 @@
      [(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
      [_ (continue<: A t1 t2 obj)])]
   [(case: Some (Some: _ _)) #f]
-  [(case: Struct (Struct: nm1 parent1 flds1 proc1 _ _ properties))
+  [(case: Struct (Struct: nm1 parent1 flds1 extras1 _ _ properties))
    (match t2
      ;; Avoid resolving things that refer to different structs.
      ;; Saves us from non-termination
@@ -1213,12 +1213,14 @@
       #:when (unrelated-structs t1 t2)
       #f]
      ;; subtyping on immutable structs is covariant
-     [(Struct: nm2 _ flds2 proc2 _ _ _)
+     [(Struct: nm2 _ flds2 extras2 _ _ _)
       #:when (free-identifier=? nm1 nm2)
       (let ([A (remember t1 t2 A)])
         (with-updated-seen A
-          (let ([A (cond [(and proc1 proc2) (subtype* A proc1 proc2)]
-                         [proc2 #f]
+          (let ([A (cond [(and extras1 extras2) (for/and ([et1 (in-list extras1)]
+                                                          [et2 (in-list extras2)])
+                                                  (subtype* A et1 et2))]
+                         [extras2 #f]
                          [else A])])
             (for/fold ([A A])
                       ([f1 (in-list flds1)]
diff --git a/typed-racket-test/succeed/prop-evt.rkt b/typed-racket-test/succeed/prop-evt.rkt
new file mode 100644
index 000000000..3cf16925b
--- /dev/null
+++ b/typed-racket-test/succeed/prop-evt.rkt
@@ -0,0 +1,62 @@
+#lang typed/racket/base
+
+(define ch ((inst make-channel Number)))
+
+
+(struct aaa0 ((evt : (Channelof Number)))
+  #:property prop:evt (struct-field-index evt))
+
+(thread (lambda ()
+          (channel-put ch 10)))
+
+(ann (sync (aaa0 ch)) Number)
+
+
+(struct aaa1 ([evt : (Evtof Number)])
+  #:property prop:evt 0)
+
+(thread (lambda ()
+          (channel-put ch 10)))
+
+(ann (sync (aaa1 ch)) Number)
+
+(struct aaa2 ([evt : (Channelof Number)])
+  #:property prop:evt (lambda ([self : aaa2]) : (Channelof Number)
+                        (aaa2-evt self)))
+
+(thread (lambda ()
+          (channel-put ch 10)))
+(ann (sync (aaa2 ch)) Number)
+
+
+(define ch2 ((inst make-channel String)))
+(struct aaa3 ()
+  #:property prop:evt (ann ch2 (Channelof String)))
+
+(thread (lambda ()
+          (channel-put ch2 "10")))
+
+(ann (sync (aaa3)) String)
+
+
+(struct aaa4 ([b : String]) #:property prop:evt (lambda (self) : Number
+                                                  (string-length (aaa4-b self))))
+
+(ann (sync (aaa4 "hello")) aaa4)
+
+
+(struct (A) poly-aaa ([b : A]) #:property prop:evt (lambda (self) : A
+                                                     (poly-aaa-b self)))
+
+(ann (sync (poly-aaa "hello")) (poly-aaa String))
+
+(thread (lambda ()
+          (channel-put ch 10)))
+(ann (sync (poly-aaa ch))  Number)
+
+
+(struct aaa-never ([b : String]) #:property prop:evt (struct-field-index b))
+
+((lambda ([a : (Evtof Nothing)]) : String
+   "42")
+ (aaa-never "84"))
diff --git a/typed-racket-test/succeed/struct-props.rkt b/typed-racket-test/succeed/struct-props.rkt
index 840023ad8..6d843b458 100644
--- a/typed-racket-test/succeed/struct-props.rkt
+++ b/typed-racket-test/succeed/struct-props.rkt
@@ -20,9 +20,8 @@
 (struct foobar foo ([y : Number])
   #:property prop:custom-write
   (lambda ([self : foo] [p : Output-Port] [m : (U Boolean 1 0)]) : Void
-          (displayln (+ (foo-x self) 20) p))
+    (displayln (+ (foo-x self) 20) p))
   #:property prop:evt 0
-
   #:property prop:custom-print-quotable 'always)
 
 (struct foobar^ foo ([y : Number])
@@ -30,7 +29,7 @@
   (lambda ([self : foobar^] [p : Output-Port] [m : (U Boolean 1 0)]) : Void
           (displayln (+ (foobar^-y self) 20) p))
 
-  #:property prop:evt (make-channel)
+  #:property prop:evt (ann (make-channel) (Evtof Any))
 
   #:property prop:custom-print-quotable 'self)
 
diff --git a/typed-racket-test/unit-tests/contract-tests.rkt b/typed-racket-test/unit-tests/contract-tests.rkt
index 9d54755d9..89a57e3a5 100644
--- a/typed-racket-test/unit-tests/contract-tests.rkt
+++ b/typed-racket-test/unit-tests/contract-tests.rkt
@@ -223,7 +223,7 @@
             (-> -Symbol -Symbol))
            "two cases of arity 1")
    (t/fail (-struct #'struct-name2 #f (list (make-fld -Symbol #'acc #f)) (-> -Symbol))
-           "procedural structs are not supported")
+           "structs with prop:procedure or prop:evt attached are not supported")
    (t/fail (-Syntax (-> -Boolean -Boolean))
            "required a flat contract but generated a chaperone contract")
    (t/fail (-Syntax (-seq -Boolean))