Hello, is it possible to solve this goal by `exact IHDC_Proof`

?

```
1 subgoal
D, G : LCtx
n : nat
A, B : Formula
H : D ∥ G, (n -: A) ⊢s B
IHDC_Proof : [D ∥ G, (n -: A) ⊢ B] ▷+ nil
______________________________________(1/1)
[D ∥ newHypo G A ⊢ B] ▷+ nil
```

I know that the newHypo function should simplify to something as the term in IHDC_Proof, but using exact tactic is not able to know it, is it possible?

The exact tactic understands unification, so if exact does not work the two terms are not unifiable.

You can see what e.g. `Eval cbv in (newHypo G A)`

evaluates to - maybe replace cbv with simple, hnf or cbn if cbv evaluates too much.

You can also use the `change`

tactic to replace a term with a unifiable term - I use this frequently to see if two terms are indeed unifiable. Say something like `change (newHypo G A) with (G, (n -: A))`

(I don't know the syntax you use, so I am just guessing).

Finally it might help to switch off notations - sometimes notations give wrong impressions on what the term structure (associativity, ..) is.

Last updated: Sep 23 2023 at 14:01 UTC