Commit 2022-02-23 21:42 2c74921e
View on Github →feat(data/pfun): A new induction on pfun.fix (#12109)
A new lemma that lets you prove predicates given b ∈ f.fix a if f preserves the predicate, and it holds for values which f maps to b.
feat(data/pfun): A new induction on pfun.fix (#12109)
A new lemma that lets you prove predicates given b ∈ f.fix a if f preserves the predicate, and it holds for values which f maps to b.