Changeset 2307 for src/ASM/Util.ma


Ignore:
Timestamp:
Aug 30, 2012, 4:47:58 PM (7 years ago)
Author:
campbell
Message:

Half the proofs for sound cost labelling check.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2286 r2307  
    13851385qed.
    13861386
     1387lemma Prop_notb : ∀b:bool. notb b → Not (bool_to_Prop b).
     1388* /2/
     1389qed.
     1390
    13871391lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    13881392 *; /2 by eq_true_false, I/
Note: See TracChangeset for help on using the changeset viewer.