Ignore:
Timestamp:
May 9, 2012, 6:30:41 PM (8 years ago)
Author:
campbell
Message:

Tidy up labelling simulation stuff a bit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1713 r1930  
    4646[ //
    4747| #H' @False_ind @(absurd … H H')
    48 ] qed.
    49 
    50 lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
    51 #P #f #p #Q #H cases f;
    52 [ @H
    53 | #np cut False [ @(absurd ? p np) | * ]
    54 ] qed.
    55 
    56 lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
    57 #P #f #p #Q #H cases f;
    58 [ #np cut False [ @(absurd ? np p) | * ]
    59 | @H
    6048] qed.
    6149
Note: See TracChangeset for help on using the changeset viewer.