diff --git a/MyUtils.v b/MyUtils.v new file mode 100644 index 0000000..46f26af --- /dev/null +++ b/MyUtils.v @@ -0,0 +1 @@ +Ltac inv H := inversion H; clear H; subst.