Changeset 3563 for LTS/utils.ma

Timestamp:

Jun 16, 2015, 4:00:03 PM (6 years ago)

Author:

sacerdot

Message:

bind_inversion on Opt moved to utils + some progress

File:

• LTS/utils.ma (modified) (1 diff)

LTS/utils.ma

@@ -17 +17 @@
 include "../src/ASM/Util.ma".
 include "../src/utilities/option.ma".
+
+lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
+∀f : A → option B.∀y : B.
+! x ← m; f x = return y → 
+∃ x.(m = return x) ∧ (f x = return y).
+#A #B * [| #a] #f #y normalize #EQ [destruct]
+%{a} %{(refl …)} //
+qed.
 
 (*NO DUPLICATES in lists*)