在“精益”中寻找满足特定要求的操作

问：

我已经定义了四个布尔运算：

def bnot : bool → bool 
| tt := ff
| ff := tt 

def band : bool → bool → bool 
| tt b := b
| ff b := ff

def bor : bool → bool → bool 
| tt b := tt
| ff b := b

def is_tt : bool → Prop 
| tt := true
| ff := false

现在我需要定义一个新操作：

def exb  (f : bool → bool) : bool
    :=sorry,

然后使用上面的运算来计算并证明布尔值的存在性量化

exb_ok : ∀ f : bool → bool, is_tt (exb f) ↔ ∃ x : bool, is_tt (f x) :=
begin
  sorry,
end 

现在将“对不起”更改为真正的答案。

我想可能是它有

def exb  (f : bool → bool) : bool
    := f tt || f ff

theorem exb_ok : ∀ f : bool → bool, is_tt (exb f) ↔ ∃ x : bool, is_tt (f x) :=
begin
  assume f,
  constructor,
  dsimp[exb],
  assume h,
  existsi tt,
end

我停在这一步，我不知道下一步该怎么做。 现在的目标是

'f : bool → bool,
 h : is_tt (f tt||f ff)
 ⊢ is_tt (f tt)
 
 f : bool → bool
 ⊢ (∃ (x : bool), is_tt (f x)) → is_tt (exb f)'