Make proofs of existence smoother #87
Description
Global facts formulated with obtains with one alternative and local facts formulated with obtain have the form (⋀x. P x ⟹ Q x ⟹ … ⟹ thesis) ⟹ thesis. Often, we prove such facts by showing ?thesis, which is thesis, using the local fact that, which is ⋀x. P x ⟹ Q x ⟹ … ⟹ thesis. However, the standard proof method, which is in particular invoked when proof comes with no initial proof method, turns such an eliminator-style goal into the subgoals (⋀x. P x ⟹ Q x ⟹ … ⟹ thesis) ⟹ P ?x, (⋀x. P x ⟹ Q x ⟹ … ⟹ thesis) ⟹ Q ?x, etc., which are weaker variants of P ?x, Q ?x, etc. Therefore, it is possible to not put - after proof and then just pick a concrete witness x and show P x, Q x, etc. individually, instead of putting - after proof and proving the whole eliminator-style fact, which involves referring to that. This alternative approach generally results in smoother proofs. We shall correspondingly change proofs of facts of the above-mentioned form wherever this improves the readability of the code.