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: Nov 29 2023 at 21:01 UTC