Great!. This worked perfectly and solved some persistent issues...:)
On Tue, Aug 28, 2018 at 12:54 AM wrote:
> Don’t use abbreviations before starting your proof: it’s muddling your
> quantifications.
>
> Instead, use
>
>!s. (?s0. s = StreamD s0) /\ P s ==> streams A s
>
> as your goal and
Don’t use abbreviations before starting your proof: it’s muddling your
quantifications.
Instead, use
!s. (?s0. s = StreamD s0) /\ P s ==> streams A s
as your goal and follow with
ho_match_mp_tac streams_coind >> dsimp[]
You will then end up with
∀s0.
P (StreamD s0) ⇒
∃a s0
