blob: 42cb2309e02fbbb11f55415e6c5c8ff79c472743 (
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
27
28
29
30
31
32
|
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
fun b c : bool => b = c
: bool -> bool -> Prop
fun c b : bool => b = c
: bool -> bool -> Prop
fun b1 b2 => b1 = b2
: bool -> 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
|
