blob: aeb975b59a2db30ba83a31132b0c48087516fad6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Inversion H.
Absurd (Ex [a:b] c).
Discriminate H.
DEq 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).
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) ] in v.
Hint Rewrite <- [ (A b) ] in v using Auto.
|
