fact: Definition p2 : package fset0 [interface] I2 := [package #def #[4] (x : 'bool × 'bool) : 'bool { let '(u,v) := x in ret v } ].
imports: Coq(Utf8) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) extructures(ord fset fmap) Crypt(RulesStateProb Package Prelude) Equations(Equations)