From c8111d23ce440787ca43a0b17faf902a2c620d85 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 1 Feb 2017 16:51:39 -0500 Subject: Add inversion_expr --- src/Util/Sigma.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src/Util/Sigma.v') diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 9259e1a1d..57c82df68 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -221,12 +221,14 @@ Ltac simpl_proj_exist_in H := | context G[projT2 (existT _ ?x ?p)] => let G' := context G[p] in change G' in H end. -Ltac induction_sigma_in_using H rect := - let H0 := fresh H in - let H1 := fresh H in +Ltac induction_sigma_in_as_using H H0 H1 rect := induction H as [H0 H1] using (rect _ _ _ _); simpl_proj_exist_in H0; simpl_proj_exist_in H1. +Ltac induction_sigma_in_using H rect := + let H0 := fresh H in + let H1 := fresh H in + induction_sigma_in_as_using H H0 H1 rect. Ltac inversion_sigma_step := match goal with | [ H : _ = exist _ _ _ |- _ ] -- cgit v1.2.3