mini-mission accomplished: confluence proved!

I learned a lot of lessons including how to circumvent the strict positivity checks in coq:

I defined seq_forall_pair as:

```
Definition seq_forall_pair A B (R: A -> B -> Prop) s1 s2 :=
size s1 = size s2 /\ forall ts, PIn ts (zip s1 s2) -> R (ts.1) (ts.2).
```

And I used this everywhere instead of what I had before, also it was good exercise in writing custom induction principles for reduction and conversion.

once again thanks a lot for all the help and the idea.

walker has marked this topic as resolved.

Last updated: Aug 02 2024 at 23:01 UTC