File: siprop.ref

package info (click to toggle)
coq-iris 4.3.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 4,116 kB
  • sloc: python: 130; makefile: 61; sh: 28; sed: 2
file content (17 lines) | stat: -rw-r--r-- 499 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
 
"unseal_test"
     : string
1 goal
  
  P, Q : siProp
  Φ : nat → siProp
  ============================
  siprop.siProp_and_def P
    (siprop.siProp_and_def (siprop.siProp_later_def Q)
       (siprop.siProp_exist_def (λ x : nat, Φ x)))
  ⊣⊢ siprop.siProp_exist_def
       (λ x : nat,
          siprop.siProp_or_def
            (siprop.siProp_and_def P
               (siprop.siProp_and_def (siprop.siProp_later_def Q)
                  (siprop.siProp_pure_def True))) 
            (Φ x))