# Re: [isabelle] Meta_impE and other tactics

Hi Peter,
your reasoning is not sound: Take, e.g., A=B=C=False, and D=E=True.
Then, your goal reads

`[| [| False ; False |] ==> False ; True ; True ; False ==> True ; False
``==> True |] ==> False
`
which simplifies to False, whereas you want to rewrite this to
[| [| True; True |] ==> False; True; True |] ==> False

`which is True. The problem is that you need both A and B to show C, but
``you only have D and E, which are weaker than A and B.
`
Best regards,
Andreas
Peter Chapman schrieb:

Hi

`I have the following premisses and goal (the details are unimportant, it
``is the structure which is important):
`
[| [| A ; B |] ==> C ; D ; E ; A ==> D ; B ==> E |] ==> C

`I think this should be provable, I rewrite using the A ==> D and B ==> E
``inside the inner [| |] to get
`
[| [| D ; E |] ==> C ; D ; E |] ==> C
to
C

`Is this logically sound? How can I rewrite the A and B within the inner
``brackets?
`
Thanks in advance
Peter

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*