Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rodolphe Lepigre
Iris
Commits
d5c0458f
Commit
d5c0458f
authored
Jun 27, 2019
by
Robbert Krebbers
Browse files
Up to 12 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`.
Created this commit with pain in my heart!
parent
57e5d1ed
Changes
1
Show whitespace changes
Inline
Side-by-side
theories/proofmode/ltac_tactics.v
View file @
d5c0458f
...
...
@@ -626,6 +626,20 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
:
=
iForallRevert
x8
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
:
=
iForallRevert
x9
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
:
=
iForallRevert
x10
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
:
=
iForallRevert
x11
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
:
=
iForallRevert
x12
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
")"
constr
(
Hs
)
:
=
iRevert
Hs
;
iRevert
(
x1
).
...
...
@@ -648,6 +662,21 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
constr
(
Hs
)
:
=
iRevert
Hs
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
constr
(
Hs
)
:
=
iRevert
Hs
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
constr
(
Hs
)
:
=
iRevert
Hs
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
constr
(
Hs
)
:
=
iRevert
Hs
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
).
Tactic
Notation
"iRevert"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
constr
(
Hs
)
:
=
iRevert
Hs
;
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
).
(** * The specialize and pose proof tactics *)
Record
iTrm
{
X
As
S
}
:
=
...
...
@@ -1649,6 +1678,26 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
constr
(
Hs
)
"with"
tactic3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
constr
(
Hs
)
"with"
tactic3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
constr
(
Hs
)
"with"
tactic3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
constr
(
Hs
)
"with"
tactic3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
constr
(
Hs
)
"with"
tactic3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)).
Tactic
Notation
"iRevertIntros"
"with"
tactic3
(
tac
)
:
=
iRevertIntros
""
with
tac
.
...
...
@@ -1674,6 +1723,21 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
"with"
tactic3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
"with"
tactic3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
"with"
tactic3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
"with"
tactic3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
"with"
tactic3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)
""
with
tac
.
(** * Destruct tactic *)
Class
CopyDestruct
{
PROP
:
bi
}
(
P
:
PROP
).
...
...
@@ -1895,37 +1959,63 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
iRevertIntros
(
x1
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
constr
(
Hs
)
:
=
...
...
@@ -1933,39 +2023,66 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)
""
with
(
iInductionCore
(
induction
x
as
pat
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
:
=
...
...
@@ -1973,39 +2090,69 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
iRevertIntros
(
x1
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
:
=
iInductionRevert
x
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
constr
(
Hs
)
:
=
...
...
@@ -2013,39 +2160,68 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
Tactic
Notation
"iInduction"
constr
(
x
)
"as"
simple_intropattern
(
pat
)
constr
(
IH
)
"using"
uconstr
(
u
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
constr
(
Hs
)
:
=
iInductionRevert
x
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)
""
with
(
iInductionCore
(
induction
x
as
pat
using
u
)
as
IH
)).
(** * Löb Induction *)
Tactic
Notation
"iLöbCore"
"as"
constr
(
IH
)
:
=
...
...
@@ -2071,53 +2247,91 @@ Tactic Notation "iLöbRevert" constr(Hs) "with" tactic3(tac) :=
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
:
=
iL
ö
bRevert
""
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
ident
(
x9
)
ident
(
x10
)
ident
(
x11
)
ident
(
x12
)
")"
:
=
iL
ö
bRevert
""
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
constr
(
Hs
)
:
=
iL
ö
bRevert
Hs
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
")"
constr
(
Hs
)
:
=
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
")"
constr
(
Hs
)
:
=
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
x2
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
x2
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
constr
(
Hs
)
:
=
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
x2
x3
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
constr
(
Hs
)
:
=
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
)
""
with
(
iL
ö
bCore
as
IH
)).
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
"forall"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
constr
(
Hs
)
:
=
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
(
iL
ö
bCore
as
IH
)).
iL
ö
bRevert
Hs
with
(
iRevertIntros
(
x1
x2
x3
x4
x5
<