I'm quite new to Coq, I have done several projects in OCaml before and I'm doing this as a preparation for a course I'm taking next semester.
A friend recommended the exercise of proofing the deduction theorem and I'm having trouble with a few steps. One thing is still giving me trouble.
I'm trying to prove this, where ac is just an inductive type with a context and a formula:
ac Gamma (Impl alpha beta) -> ac (alpha :: Gamma) beta.```
After applying modus ponens, I get the first subgoal:
ax (alpha :: Gamma) (Impl alpha beta)
with H:
ax Gamma (Impl alpha beta)
My understanding is that the context is only stronger with alpha :: Gamma so it is automatically true, my next thought was that coq would recognize this and I could just do exact H. and finish this subgoal, but it says it can't match those.
Why does it does not work? I just don't see why this would not be true.
