blob: 824c260e92f5793ccbe337f2e5aa56fc3276855a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
forall b, b = b
: Prop
forall b : nat, b = b
: Prop
forall b : bool, @eq bool b b
: Prop
forall b : bool, b = b
: Prop
forall b c : bool, b = c
: Prop
forall c b : bool, b = c
: Prop
forall b1 b2, b1 = b2
: Prop
fun b => b = b
: bool -> Prop
fix f b (n : nat) {struct n} : bool :=
match n with
| 0 => b
| S p => f b p
end
: bool -> nat -> bool
∀ b c : bool, b = c
: Prop
∀ b1 b2, b1 = b2
: Prop
|
