blob: 6cdbdd13f682bcc945fc22e84639df4fddb18af7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
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.
Hint Rewrite -> [ (A b) ] in v.
Hint Rewrite <- [ (A b) ] in v using Auto.
|
