blob: 2fce00f9fd13235b3267bb43cf1b9672c4d038fe (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Theorem foo (b:bool) : b = true \/ b = false.
Proof.
Fail dependent destruction b.
Fail dependent induction b.
Abort.
From Coq Require Import Program.Equality.
Theorem foo_with_destruction (b:bool) : b = true \/ b = false.
Proof.
dependent destruction b; auto.
Qed.
Theorem foo_with_induction (b:bool) : b = true \/ b = false.
Proof.
dependent induction b; auto.
Qed.
|
