Inductive Set Construction using Instantiation and Rodin, D. Cansell
https://wiki.event-b.org/images/202606.pdf All proof obigations of my Rodin workshop paper are in Rodin2026 in this archive You need the context instantiation plugin (pleased asked to Yamine Ait Ameur). Only automatic proofs are green. Have fun! There are no comment then no english then no bad english. For my talk I've presented in this following order DemoListwfix (I've instantated fixpoint). It's Listwithfix. List EquivList: if I've 2 elements in List or on different Lists they are equivalent. SeqIsList (where I've used sequence defined by Jean-Raymond). FrLB to define recursive function on lists ms FrLSB similar then FrLB but with another parameter Lordwithfix insert sort proof_insert proof_sort I left my cave in 2020 for Jean-Raymond. It's time I went back. My Rodin presentation will be the last one. Jean-Raymond today it's the first year without you (May 26 2026). I feel an immense emptiness since you left. I loose my favorite problems dealer....