I add finite conjectures for two implications that Terence proved on Zulip and a set that I have been able to verify using Duper but not yet been able to convert the Vampire proofs for.
Also just wanted to note that while the list looks a bit long, this is due to not having the Facts syntax and the conjectures have been transitively reduced.
I add finite conjectures for two implications that Terence proved on Zulip and a set that I have been able to verify using Duper but not yet been able to convert the Vampire proofs for.
See https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/481257624