!! 仮定の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 ============================ で,destruct H1 as [a [H2 {{e #124}} H3]] とすると,2つのゴールができる: a : A H2 : P a ============================ a : A H3 : Q a ============================