fact: Definition test₄ : package fset0 [interface] _ := [package #def #[ 0 ] (n : 'nat) : 'nat { ret (n + n)%N } ; #def #[ 1 ] (b : 'bool) : 'nat { if b then ret 0 else ret 13 } ].
imports: Coq(Utf8) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) extructures(ord fset fmap) Crypt(RulesStateProb Package Prelude) Equations(Equations)