[rudynicolop]

Relates to ITree PR 285.

As per the discussion on zulip

• https://rocq-prover.zulipchat.com/#narrow/channel/394939-Interaction-Trees/topic/coinduction.20plugin/near/608989582

[rogerburtonpatel]

If this builds, great! If the change to the signature of ruttF breaks things down the line, I recommend using Arguments to fix it as in Eqit.v, line 166 and around. You may have to play with context variables to get it working nicely.

[rudynicolop]

If this builds, great! If the change to the signature of ruttF breaks things down the line, I recommend using Arguments to fix it as in Eqit.v, line 166 and around. You may have to play with context variables to get it working nicely.

I have the argument order of rutt match ruttF, rutt_, and rutt_mon, by the recommendation of @YaZko. I have separate Proper instances, but the proofs are not replicated.

Here I preserve the original Section in Rutt.v.

[rudynicolop]

If this builds, great!

I believe that this builds 😅 (I only checked on my local setup)