blob: 7d60bbd97785362903b7441f99e26ac98c16e1e3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
inversion H.
try absurd (exists a : b, c).
discriminate H.
simplify_eq H.
injection H.
replace a with b.
rewrite <- H with (a := b).
rewrite <- H with (a := b) in H1.
conditional (auto) rewrite H with (1 := b).
conditional (auto) rewrite H with (1 := b) in H2.
dependent rewrite H.
cutrewrite (a = b).
cutrewrite (a = b) in H.
eauto 3 4 with a.
prolog [ A (B c) ] 4.
eapply H with (1 := H2) (a := b).
inversion H using (A b).
inversion H using (A b) in H1 H2.
ring a b.
Hint Rewrite -> (A b) : v.
Hint Rewrite <- (A b) using auto : v.
|
