- 追加された行はこのように表示されます。
- 削除された行は
このように表示されます。
!! 仮定のexistsをinstantiateする
destruct タクティックの,disj_conj_intro_pattern というのを使う.
例:
H1 : exists x : A, P x
=======
で,destruct H1 as [a H2] とすると
a : A
H2 : P a
=======
となる.同様に,
H1 : exists x : A, P x /\ Q x
============================
で,destruct H1 as [a [H2 H3]] とすると,
a : A
H2 : P a
H3 : Q a
============================
となる.また,
H1 : exists x : A, P x \/ Q x
============================
{{e #124}}
{{e #42}}
{{e #42}}
で,destruct H1 as [a [H2 {{e #124}} H3]]
とすると,2つのゴールができる:
a : A
H2 : P a
============================
a : A
H3 : Q a
============================