Changeset 3563 for LTS/utils.ma


Ignore:
Timestamp:
Jun 16, 2015, 4:00:03 PM (6 years ago)
Author:
sacerdot
Message:

bind_inversion on Opt moved to utils + some progress

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/utils.ma

    r3554 r3563  
    1717include "../src/ASM/Util.ma".
    1818include "../src/utilities/option.ma".
     19
     20lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
     21∀f : A → option B.∀y : B.
     22! x ← m; f x = return y →
     23∃ x.(m = return x) ∧ (f x = return y).
     24#A #B * [| #a] #f #y normalize #EQ [destruct]
     25%{a} %{(refl …)} //
     26qed.
    1927
    2028(*NO DUPLICATES in lists*)
Note: See TracChangeset for help on using the changeset viewer.