2 files changed, 46 insertions, 7 deletions

diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index ecffbad97..2c2533454 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -52,7 +52,8 @@ Section language.
     repeat first [ intro
                  | progress simpl in *
                  | reflexivity
-                 | tauto
+                 | assumption
+                 | progress destruct_head False
                  | progress subst
                  | progress inversion_option
                  | progress inversion_sigma
@@ -70,23 +71,23 @@ Section language.
 
   Lemma invert_Const_Some {t e v}
     : @invert_Const t e = Some v -> e = Const v.
-  Proof. t. Qed.
+  Proof. t. Defined.
 
   Lemma invert_Var_Some {t e v}
     : @invert_Var t e = Some v -> e = Var v.
-  Proof. t. Qed.
+  Proof. t. Defined.
 
   Lemma invert_Op_Some {t e v}
     : @invert_Op t e = Some v -> e = Op (fst (projT2 v)) (snd (projT2 v)).
-  Proof. t. Qed.
+  Proof. t. Defined.
 
   Lemma invert_LetIn_Some {t e v}
     : @invert_LetIn t e = Some v -> e = LetIn (fst (projT2 v)) (snd (projT2 v)).
-  Proof. t. Qed.
+  Proof. t. Defined.
 
   Lemma invert_Pair_Some {A B e v}
     : @invert_Pair A B e = Some v -> e = Pair (fst v) (snd v).
-  Proof. t. Qed.
+  Proof. t. Defined.
 End language.
 
 Global Arguments invert_Const {_ _ _ _ _} _.
diff --git a/src/Util/Option.v b/src/Util/Option.v
index 82ddf6750..64bdb4197 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -109,14 +109,52 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect
          end.
 
 Definition option_leq_to_eq {A} (x y : option A) : x = y -> option_eq eq x y.
-Proof. destruct x; intro; subst; simpl; reflexivity. Qed.
+Proof. destruct x; intro; subst; simpl; reflexivity. Defined.
+
+Definition option_eq_to_leq {A} (x y : option A) : option_eq eq x y -> x = y.
+Proof.
+  destruct x, y; simpl;
+    try solve [ intros []
+              | apply f_equal
+              | reflexivity
+              | apply eq_sym ].
+Defined.
+
+Lemma option_leq_to_eq_to_leq {A x y} v : @option_eq_to_leq A x y (@option_leq_to_eq A x y v) = v.
+Proof.
+  destruct x; subst; simpl; reflexivity.
+Qed.
+
+Lemma option_eq_to_leq_to_eq {A x y} v : @option_leq_to_eq A x y (@option_eq_to_leq A x y v) = v.
+Proof.
+  compute in *.
+  repeat first [ progress subst
+               | progress break_match
+               | reflexivity ].
+Qed.
+
+Lemma UIP_None {A} (p q : @None A = @None A) : p = q.
+Proof.
+  rewrite <- (option_leq_to_eq_to_leq p), <- (option_leq_to_eq_to_leq q); simpl; reflexivity.
+Qed.
+
+Lemma invert_eq_Some {A x y} (p : Some x = Some y) : { pf : x = y | @option_eq_to_leq A (Some x) (Some y) pf = p }.
+Proof.
+  eexists; apply option_leq_to_eq_to_leq.
+Qed.
 
 Ltac inversion_option_step :=
   match goal with
   | [ H : Some _ = Some _ |- _ ] => apply option_leq_to_eq in H; unfold option_eq in H
+  | [ H : Some _ = Some _ |- _ ]
+    => let H' := fresh in
+       rename H into H';
+       destruct (invert_eq_Some H') as [H ?]; subst H'
   | [ H : None = Some _ |- _ ] => solve [ inversion H ]
   | [ H : Some _ = None |- _ ] => solve [ inversion H ]
   | [ H : None = None |- _ ] => clear H
+  | [ H : None = None |- _ ]
+    => assert (eq_refl = H) by apply UIP_None; subst H
   end.
 
 Ltac inversion_option := repeat inversion_option_step.