Changeset 3563 for LTS/Vm.ma


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

bind_inversion on Opt moved to utils + some progress

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3552 r3563  
    33include "../src/utilities/option.ma".
    44include "basics/jmeq.ma".
    5 
    6 lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
    7 ∀f : A → option B.∀y : B.
    8 ! x ← m; f x = return y →
    9 ∃ x.(m = return x) ∧ (f x = return y).
    10 #A #B * [| #a] #f #y normalize #EQ [destruct]
    11 %{a} %{(refl …)} //
    12 qed.
    135
    146record assembler_params : Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.