Julia Dijkstra has marked this topic as resolved.

I still had to resort to doing this to rewrite , since the tactic did not work.

```
Theorem norm_neg_correct: forall (p: form) (V: valuation), valid' V (norm_neg p) = valid' V p.
Lemma norm_neg_correct_fun: forall (p: form),
(fun V => valid' V (norm_neg p)) = (fun V => valid' V p).
Proof.
intros. apply functional_extensionality. intros. apply norm_neg_correct.
Qed.
```

Last updated: Jun 23 2024 at 04:03 UTC