| changeset 11635 | fd242f857508 |
| parent 11591 | 4b171ad4ff65 |
| child 14981 | e73f8140af78 |
| 11634:cddf6441a14a | 11635:fd242f857508 |
|---|---|
50 proof |
50 proof |
51 assume "?P = ?Q" |
51 assume "?P = ?Q" |
52 hence "Eps ?P = Eps ?Q" by (rule arg_cong) |
52 hence "Eps ?P = Eps ?Q" by (rule arg_cong) |
53 also note P |
53 also note P |
54 also note Q |
54 also note Q |
55 finally have "False = True" . |
55 finally show False by (rule False_neq_True) |
56 thus False by (rule False_neq_True) |
|
57 qed |
56 qed |
58 have "\<not> A" |
57 have "\<not> A" |
59 proof |
58 proof |
60 assume a: A |
59 assume a: A |
61 have "?P = ?Q" |
60 have "?P = ?Q" |