10 lines
169 B
Text
10 lines
169 B
Text
|
open bool
|
||
|
|
definition is_equiv_bnot : is_equiv bnot :=
|
||
|
|
begin
|
||
|
|
fapply is_equiv.mk,
|
||
|
|
exact bnot,
|
||
|
|
all_goals (intro b;cases b),
|
||
|
|
state,
|
||
|
|
repeat reflexivity
|
||
|
|
end
|