/- 用語： スタブ： from https://e-words.jp/w/%E3%82%B9%E3%82%BF%E3%83%96.html
スタブとは、切り株、半券、（何かが減ったり短くなった）残り、などの意味を持つ英単語。ITの分野では、本物が用意できないときに動作に支障が無いようにとりあえず置いておく代用品という意味で用いられることが多い。
-/
variable {A B:Prop}
/- 一部後回しにした暫定版 -/
def main_?
(left_? : A → B) (right_? : B → A) -- スタブ（後回しにした部分）
: A ↔ B
:= Iff.intro left_? right_?
#check main_?
/- バックログは left_?, right_? -/
/- ここでスタブに証明を与える
バックログの解消
-/
def left : A → B := sorry
def right : B → A := sorry
/- スタブを埋めた完成版 -/
def main : A ↔ B
:= main_? left right
